Commit 13ff886d9bddc167b6f7decc35c78185e4e85c0b

  • avatar
  • Ville Tirronen <ville.tirronen @j…u.fi> (Committer)
  • Fri Aug 24 14:54:41 EEST 2018
  • avatar
  • Ville Tirronen <ville.tirronen @j…u.fi> (Author)
  • Fri Aug 24 14:54:41 EEST 2018
WIP
DerivationChecker/DCService/src/Service.hs
(6 / 5)
  
9999 Left derivation -> pure (taskPage (toElm derivation))
100100 Right typing -> liftIO (print (Aeson.encode (typingToElm typing))) >> pure (typingTaskPage (typingToElm typing))
101101
102
102103 serveTypeCheck user taskName request = do
103 response <- case Typing.serverReply Typing.allRules request of
104 Left e -> throwError err400
105 { errBody = LT.encodeUtf8 $ Typing.prettyPrintTypeConversionError e
106 }
107 Right resp -> pure resp
104 let fn = tasksAt conf <> "/" <> taskName
105 let ppErr e = throwError err400 { errBody = LT.encodeUtf8 $ Typing.prettyPrintTypeConversionError e }
106 tf <- liftIO $ Dhall.detailed $ Dhall.input Dhall.auto fn
107 aas <- either ppErr pure (traverse parseAcceptedAnswer (accepts tf))
108 response <- either ppErr pure (Typing.serverReply aas Typing.allRules request)
108109 case user of
109110 Failure -> do
110111 liftIO
DerivationChecker/DCServiceAPI/src/DerivationChecker/API.hs
(8 / 0)
  
77{-# LANGUAGE OverloadedStrings #-}
88{-# LANGUAGE TypeOperators #-}
99{-# LANGUAGE TemplateHaskell #-}
10{-# LANGUAGE TupleSections #-}
1011{-# LANGUAGE ScopedTypeVariables #-}
1112
1213module DerivationChecker.API where
3434
3535data CheckStep = Check String String deriving (Generic,Eq,Show)
3636
37data AcceptedAnswer a = AcceptedAnswer {acceptsType::a,msg::String} deriving (Eq,Show,Generic)
38parseAcceptedAnswer :: AcceptedAnswer Text -> Either Typing.TypeConversionError (Typing.T,String)
39parseAcceptedAnswer (AcceptedAnswer a m) = (,m) <$> Typing.parseEasyTE (Text.unpack a)
40
41
3742data TypeTaskFlags
3843 = TTF {t_question :: Text
3944 ,t_expression :: Text
4045 ,knownInstances :: [Text]
46 ,accepts :: [AcceptedAnswer Text]
4147 } deriving (Generic,Eq,Show)
4248
4349data TaskFlags
8282
8383instance Dhall.Interpret TaskFlags where
8484instance Dhall.Interpret TypeTaskFlags where
85instance Dhall.Interpret a=>Dhall.Interpret (AcceptedAnswer a) where
8586instance Dhall.Interpret a => Dhall.Interpret (Hint a) where
8687instance Dhall.Interpret a => Dhall.Interpret (Goal a) where
8788
DerivationChecker/elms/TypeGUI.elm
(17 / 4)
  
9292 else Model {model | currentMessage = Just reply.lastReasons
9393 , currentCtx = reply.currentConstraints} ! []
9494
95 Update (Result.Err httpErr) -> Model model ! [] -- TODO! Errors must be seen!
95 Update (Result.Err (Http.BadStatus httpErr))
96 -> Model {model | currentMessage=Just (toString httpErr.body)} ! []
9697
98 Update (Result.Err httpErr) -> Model {model | currentMessage =Just ("There was an error:"++ toString httpErr ++", tell Ville!")} ! []
99
97100 Activate maddr -> case maddr of
98 Nothing -> Model {model |currentSTA = Nothing} ![]
99 Just addr -> Model {model | currentSTA = Just (T.STA (addrExprNum addr) (addrToTarget addr) "")} ! []
101 Nothing -> Model {model | currentSTA = Nothing} ![]
102 Just addr -> case model.reply of
103 Nothing -> Model {model | currentSTA = Just (T.STA (addrExprNum addr) (addrToTarget addr) "")} ! []
104 Just reply -> case findAnnotation addr reply.currentTypeAnnotations of
105 Nothing -> case model.currentSTA of
106 Nothing -> Model {model | currentSTA = Just (T.STA (addrExprNum addr) (addrToTarget addr) "")} ! []
107 Just sta -> if getAddr sta == addr then Model model ![]
108 else Model {model | currentSTA = Just (T.STA (addrExprNum addr) (addrToTarget addr) "")} ! []
109 Just existingSTA -> Model {model | currentSTA = Just existingSTA}![]
100110
101111 Undo -> Model model ! []
102112
155155 Nothing -> [])
156156
157157renderComplete mr = case mr of
158 Just r -> if r.isComplete then div [class "complete"] "Exercise complete!"
158 Just r -> if r.isComplete
159 then [div [class "complete"] [text "Exercise complete!"]]
160 else []
161 Nothing -> []
159162
160163renderConstraints : Bool -> Model -> Html Msg
161164renderConstraints editable (Model mc)
DerivationChecker/src/SubLanguage.hs
(1 / 1)
  
895895 addBrackets (FE e n xs) = FE e n (Constant "[" : xs ++ [Constant "]"])
896896 pif :: Fix (Numbering (Numbering (Expr V))) -> Fragment
897897 pif child@(Fix ((e2 :-- e2fixity) :-- _))
898 | e2fixity <= fixity = Nest $ addParens (prnt child)
898 | e2fixity < fixity = Nest $ addParens (prnt child)
899899 | otherwise = Nest $ prnt child
900900 in
901901 case e of
DerivationChecker/src/Typing.hs
(51 / 4)
  
6969-- Renaming type variables (Big rock!)
7070-- Separate hints.
7171-- Context of history element is no longer wrong in the gui
72-- Is complete should check that the type is general enough (Messages can be added to different results)
73-- Clicking on a filled annotation no longer clears the annotation
74--
75-- Show student when they is done
7276--
7377-- == Needs (Minimum) ==
7478-- Testing!
79-- Quick rule for calculating function compositions
7580-- Per exercise known types
81-- == Needs (Appreciated) ==
7682-- Cannot remove redundant constraints yet..
7783-- Avoid duplicating sta:s if user does the same thing twice
84-- forall introduction
7885
7986data T' v = Forall [v] [Constraint (T' v)] (T' v)
8087 | String
183183
184184-- This is the interface method to use in the servant api
185185serverReply
186 :: TypingRuleSet
186 :: [(T,String)]
187 -> TypingRuleSet
187188 -> ClientRequest
188189 -> Either TypeConversionError ServerReply
189serverReply rules ClientRequest{clientState=tds0,clientCommand=action} = case deserializeTDM tds0 of
190serverReply acceptedAnswers rules ClientRequest{clientState=tds0,clientCommand=action} = case deserializeTDM tds0 of
190191 Left err -> Left err
191192 Right tds -> case parseDA action of
192193 Left err -> Left err
198198 lastOrEmpty [] = mempty
199199 currentConstraints = prettyPrintConstraint . Set.toList . context $ model
200200 currentSTAs = Prelude.map (fmap prettyPrintT) . disassembleTypedAST . typedExpr $ model
201 completeStatus = checkFinalResult acceptedAnswers model
201202 in Right $ ServerReply
202203 tds0{ history0 = history0 tds0 ++ [action] }
203204 (T.unpack $ T.intercalate ", " $ Prelude.map renderTypeReason (toList reason))
206206 currentSTAs
207207 (serializeFragments . toFragments . forgetTypes . typedExpr $ model)
208208 (stepIsCorrect reason)
209 (let _ :.: tl = typedExpr model in not (F.null (expression tl)))
210 ""
209 (isJust completeStatus)
210 (maybe "" snd completeStatus)
211211
212-- Note: For simplicity, we currently check only the expression type
213checkFinalResult :: [(T,String)] -> TypeDeductionModel -> Maybe ((T,String))
214checkFinalResult ts model = find check ts
215 where
216 check aa = case typedExpr model of
217 (_ :.: tl) | Fst t₂ <- expression tl
218 , Typing.alphaEq (fst aa) t₂
219 -> True
220 _ -> False
212221
213222
223
214224autofillParensOnModel :: TypeDeductionModel -> TypeDeductionModel
215225autofillParensOnModel tdm = tdm{typedExpr=autofillParens (typedExpr tdm)}
216226
357357recoverReplacementCtx1 _ _ = Nothing
358358
359359-- NOTE: This assumes that constraints have the same ordering. Shouldn't be too much trouble...
360isCharStringEqvCtx cs₁ cs₂
361 | Prelude.length cs₁ == Prelude.length cs₂ = and (Prelude.zipWith isCharStringEqvC cs₁ cs₂)
362 | otherwise = False
363 where
364 isCharStringEqvC (Constraint c₁ t₁) (Constraint c₂ t₂) | c₁ == c₂ = isCharStringEqv t₁ t₂
365 isCharStringEqvC (TypeConstraint c₁ t₁) (TypeConstraint c₂ t₂) | c₁ == c₂ = isCharStringEqv t₁ t₂
366 isCharStringEqvC _ _ = False
367
368
369-- NOTE: This assumes that constraints have the same ordering. Shouldn't be too much trouble...
360370recoverReplacementCtx
361371 :: [Constraint T] -> [Constraint T] -> Maybe (Replacement V T)
362372recoverReplacementCtx cs₁ cs₂
401401 (Typing.Bool , Typing.Bool) -> Just emptyReplacement
402402 other -> Nothing
403403
404isCharStringEqv :: T -> T -> Bool
405isCharStringEqv a b = case (a,b) of
406 -- Interesting case
407 (Typing.String , Typing.List Typing.Char) -> True
408 (Typing.List Typing.Char , Typing.String) -> True
409 -- Recursive cases
410 (Forall vars₁ cs₁ t₁,Forall vars₂ cs₂ t₂) -> isCharStringEqv t₁ t₂ && isCharStringEqvCtx cs₁ cs₂
411
412 (Typing.List a, Typing.List b) -> isCharStringEqv a b
413 (a :$ b, a₁ :$ b₁) -> isCharStringEqv a a₁ && isCharStringEqv b b₁
414 (a :-> b, a₁ :-> b₁) -> isCharStringEqv a a₁ && isCharStringEqv b b₁
415 -- Non-recursive case:
416 (a,b) -> a==b
417
404418applyReplacement :: Replacement V T -> T -> T
405419applyReplacement r e = case e of
406420 orig@(TypeVar a) -> case getReplacement a r of
708708 | SetConstraints [ Constraint T ]
709709 | StringCharListEqv
710710 | TyVarReplacement [(V,T)]
711 | ComposeQuickHand
711712
712713 | NoIdea
713714 | NoChange
722722 | CannotSatisfyConstraints [Constraint T]
723723 | ConstraintViolations [V]
724724  | CantReplaceTypesWillyNilly T
725 | SymbolIsActually V T
725726 | SystemError String deriving (Eq,Show, Ord)
726727
727728renderTypeReason t = case t of
747747-- | SetLamBoundVarNotBoundByThis V SimpleExpr
748748 ForAllEliminationMissingConstraint constr -> format "You have dropped the constraint '{}', but I can't see why you could do that"
749749 (Only (prettyPrintConstraint [constr]))
750 SymbolIsActually (V v) t -> format "I don't think {} has that type. I think it should be {}" (v,prettyPrintT t)
750751 FreeVarUntyped (V v) t -> format "Are you trying to give {} the type {}?. To do this add '{} :: {}' before the ⊢ -symbol."
751752 (v,prettyPrintT t,v,prettyPrintT t)
752753 ForAllEliminationNotAlphaEq bs t1 t2 -> format "When eliminating foralls, you can only rename variables bound by the forAll, ie. {}"
757757 ConstraintViolations vs -> format "These variables already have a different type than what you are proposing: {}"
758758 (Only (commaSepListBy (\(V v) -> v) vs))
759759 CantReplaceTypesWillyNilly t -> format "The term you are trying to type already has a type: {}. You can only replace type variables" (Only (prettyPrintT t))
760 ComposeQuickHand -> "By function composition (eliding the details)"
760761 SystemError s -> format "Oops. This whole system had an error. Please tell Ville about this: {}" (Only s)
761762
762763commaSepListBy op = Prelude.concat . Data.List.intersperse ", " . Prelude.map op