Ismaila FALL pushed to branch track-sexp-lexp at Stefan / Typer
Commits: b97ae370 by “falismai@iro.umontreal.ca” at 2022-05-11T17:54:59+00:00 Compiler success
- - - - -
8 changed files:
- .idea/workspace.xml - src/debug.ml - src/elab.ml - src/env.ml - src/eval.ml - src/lexp.ml - src/opslexp.ml - tests/env_test.ml
Changes:
===================================== .idea/workspace.xml ===================================== @@ -1,14 +1,15 @@ <?xml version="1.0" encoding="UTF-8"?> <project version="4"> <component name="ChangeListManager"> - <list default="true" id="ae7b4cfe-7c39-4dec-88f0-41fdc6ac5172" name="Changes" comment="first"> + <list default="true" id="f42f9b4e-0225-44ed-90b7-2dfdf8c7bd73" name="Changes" comment=""> + <change beforePath="$PROJECT_DIR$/.idea/workspace.xml" beforeDir="false" /> + <change beforePath="$PROJECT_DIR$/src/debug.ml" beforeDir="false" afterPath="$PROJECT_DIR$/src/debug.ml" afterDir="false" /> <change beforePath="$PROJECT_DIR$/src/elab.ml" beforeDir="false" afterPath="$PROJECT_DIR$/src/elab.ml" afterDir="false" /> - <change beforePath="$PROJECT_DIR$/src/elexp.ml" beforeDir="false" afterPath="$PROJECT_DIR$/src/elexp.ml" afterDir="false" /> + <change beforePath="$PROJECT_DIR$/src/env.ml" beforeDir="false" afterPath="$PROJECT_DIR$/src/env.ml" afterDir="false" /> + <change beforePath="$PROJECT_DIR$/src/eval.ml" beforeDir="false" afterPath="$PROJECT_DIR$/src/eval.ml" afterDir="false" /> <change beforePath="$PROJECT_DIR$/src/lexp.ml" beforeDir="false" afterPath="$PROJECT_DIR$/src/lexp.ml" afterDir="false" /> - <change beforePath="$PROJECT_DIR$/src/log.ml" beforeDir="false" afterPath="$PROJECT_DIR$/src/log.ml" afterDir="false" /> <change beforePath="$PROJECT_DIR$/src/opslexp.ml" beforeDir="false" afterPath="$PROJECT_DIR$/src/opslexp.ml" afterDir="false" /> - <change beforePath="$PROJECT_DIR$/src/pexp.ml" beforeDir="false" afterPath="$PROJECT_DIR$/src/pexp.ml" afterDir="false" /> - <change beforePath="$PROJECT_DIR$/src/unification.ml" beforeDir="false" afterPath="$PROJECT_DIR$/src/unification.ml" afterDir="false" /> + <change beforePath="$PROJECT_DIR$/tests/env_test.ml" beforeDir="false" afterPath="$PROJECT_DIR$/tests/env_test.ml" afterDir="false" /> </list> <option name="SHOW_DIALOG" value="false" /> <option name="HIGHLIGHT_CONFLICTS" value="true" /> @@ -18,117 +19,29 @@ <component name="Git.Settings"> <option name="RECENT_GIT_ROOT_PATH" value="$PROJECT_DIR$" /> </component> - <component name="GitSEFilterConfiguration"> - <file-type-list> - <filtered-out-file-type name="LOCAL_BRANCH" /> - <filtered-out-file-type name="REMOTE_BRANCH" /> - <filtered-out-file-type name="TAG" /> - <filtered-out-file-type name="COMMIT_BY_MESSAGE" /> - </file-type-list> - </component> <component name="MarkdownSettingsMigration"> <option name="stateVersion" value="1" /> </component> - <component name="ProblemsViewState"> - <option name="selectedTabId" value="CurrentFile" /> - </component> - <component name="ProjectId" id="24oGRptlN6JcYRIGsCcefjJMNSI" /> - <component name="ProjectLevelVcsManager" settingsEditedManually="true" /> + <component name="ProjectId" id="291puQtuHyCcfq0QSMB0Wkjxvfn" /> <component name="ProjectViewState"> <option name="hideEmptyMiddlePackages" value="true" /> <option name="showLibraryContents" value="true" /> </component> - <component name="PropertiesComponent">{ - "keyToString": { - "WebServerToolWindowFactoryState": "false", - "nodejs_package_manager_path": "npm", - "settings.editor.selected.configurable": "advanced.settings" + <component name="PropertiesComponent"><![CDATA[{ + "keyToString": { + "RunOnceActivity.OpenProjectViewOnStart": "true", + "RunOnceActivity.ShowReadmeOnStart": "true" } -}</component> +}]]></component> <component name="SpellCheckerSettings" RuntimeDictionaries="0" Folders="0" CustomDictionaries="0" DefaultDictionary="application-level" UseSingleDictionary="true" transferred="true" /> <component name="TaskManager"> <task active="true" id="Default" summary="Default task"> - <changelist id="ae7b4cfe-7c39-4dec-88f0-41fdc6ac5172" name="Changes" comment="" /> - <created>1644289526498</created> + <changelist id="f42f9b4e-0225-44ed-90b7-2dfdf8c7bd73" name="Changes" comment="" /> + <created>1652290668054</created> <option name="number" value="Default" /> <option name="presentableId" value="Default" /> - <updated>1644289526498</updated> - <workItem from="1644289530024" duration="138000" /> - <workItem from="1644289685880" duration="17123000" /> - <workItem from="1644366690495" duration="2872000" /> - <workItem from="1644427616073" duration="5037000" /> - <workItem from="1644447790612" duration="354000" /> - <workItem from="1644448190692" duration="38836000" /> - <workItem from="1644604054815" duration="11794000" /> - <workItem from="1644880543067" duration="675000" /> - <workItem from="1644881233446" duration="11464000" /> - <workItem from="1644899804654" duration="21924000" /> - <workItem from="1644982629835" duration="8966000" /> - <workItem from="1645035764519" duration="8730000" /> - <workItem from="1645420768041" duration="3089000" /> - <workItem from="1645479100205" duration="14001000" /> - <workItem from="1645556924345" duration="32000" /> - <workItem from="1645556985298" duration="26618000" /> - <workItem from="1645679275172" duration="13074000" /> - <workItem from="1645747413540" duration="5456000" /> - <workItem from="1645757006612" duration="5968000" /> - <workItem from="1645854332346" duration="60370000" /> - <workItem from="1646198340389" duration="2576000" /> - <workItem from="1646240167448" duration="3710000" /> - <workItem from="1646244322960" duration="39888000" /> - <workItem from="1646332549987" duration="6206000" /> - <workItem from="1646681707621" duration="4757000" /> - <workItem from="1646688030657" duration="141913000" /> - <workItem from="1647375370648" duration="13147000" /> - <workItem from="1647401030432" duration="8445000" /> - <workItem from="1647465652106" duration="22326000" /> - <workItem from="1647533806302" duration="76666000" /> - <workItem from="1648479436675" duration="9210000" /> - <workItem from="1648489051793" duration="418000" /> - <workItem from="1648491045143" duration="14414000" /> - <workItem from="1648591752066" duration="8667000" /> - <workItem from="1648963875761" duration="8103000" /> - <workItem from="1649120540499" duration="1577000" /> - <workItem from="1649187314109" duration="50513000" /> - <workItem from="1649484792426" duration="2154000" /> - <workItem from="1649567646681" duration="1390000" /> - <workItem from="1649695892111" duration="169000" /> - <workItem from="1649803785146" duration="109628000" /> - <workItem from="1650513236334" duration="29593000" /> - <workItem from="1651015088313" duration="48549000" /> - <workItem from="1651299873584" duration="7003000" /> - <workItem from="1651596418392" duration="28840000" /> + <updated>1652290668054</updated> </task> <servers /> </component> - <component name="TypeScriptGeneratedFilesManager"> - <option name="version" value="3" /> - </component> - <component name="Vcs.Log.Tabs.Properties"> - <option name="TAB_STATES"> - <map> - <entry key="MAIN"> - <value> - <State> - <option name="FILTERS"> - <map> - <entry key="branch"> - <value> - <list> - <option value="origin/tp/ift6172-2021" /> - </list> - </value> - </entry> - </map> - </option> - </State> - </value> - </entry> - </map> - </option> - </component> - <component name="VcsManagerConfiguration"> - <MESSAGE value="first" /> - <option name="LAST_COMMIT_MESSAGE" value="first" /> - </component> </project> \ No newline at end of file
===================================== src/debug.ml ===================================== @@ -117,9 +117,9 @@ let debug_pexp_print ptop = print_info (sexp_name ptop) l ptop
let debug_lexp_decls decls = - let sep = " : " in + let sep = " : " in List.iter (fun e -> - let (((loc: sinfo), _name), lxp, _ltp) = e in + let ((loc, _name), lxp, _ltp) = e in
printf "%-15s[%s]" (lexp_name lxp) (Source.Location.to_string (sexp_location loc));
@@ -137,7 +137,7 @@ let debug_lexp_decls decls =
let str = match str with | scd :: tl - -> printf " FILE: %-25s : %s\n" (Source.Location.to_string (sexp_location loc)) scd; + -> printf " FILE: %-25s : %s\n" (sexp_location loc).file scd; tl | _ -> [] in
===================================== src/elab.ml ===================================== @@ -306,16 +306,21 @@ let elab_varref ctx (loc, name) let id = (loc, Some name) in let lxp = mkVar (id, idx) in let ltp = env_lookup_type ctx (id, idx) in + (*print_string "*************************************"; + print_string name; + print_string "***************************************"; + print_lexp_ctx (ectx_to_lctx ctx); + raise (Log.Internal_error "AIDE");*) (lxp, Inferred ltp) with Senv_Lookup_Fail xs -> (let relateds = if ((List.length xs) > 0) then ". Did you mean: " ^ (String.concat " or " xs) ^" ?" - else " " in + else " k " in sexp_error (sexp_location loc) {|The variable "%s" was not declared%s|} name relateds; - print_lexp_ctx (ectx_to_lctx ctx); - raise (Log.Internal_error "AIDE"); - (*sform_dummy_ret ctx loc*)) + (* print_lexp_ctx (ectx_to_lctx ctx); + raise (Log.Internal_error "AIDE");*) + sform_dummy_ret ctx loc)
(* Turn metavar into plain vars after generalization. * ids: an IMap that maps metavars to their position as argument @@ -622,7 +627,7 @@ and get_implicit_arg ctx loc oname t = and instantiate_implicit e t ctx = let rec instantiate t args = match OL.lexp'_whnf t (ectx_to_lctx ctx) with - | Arrow (_, ak , (_, v), t1, t2) + | Arrow (_, ((Aerasable | Aimplicit) as ak) , (_, v), t1, t2) -> let arg = get_implicit_arg ctx (lexp_sinfo e) v t1 in instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) | _ -> (mkCall (dsinfo, e, List.rev args), t) @@ -975,7 +980,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = handle_fun_args largs sargs pending ltp
(* Aerasable *) - | _, Arrow (_, ak, (_l,v), arg_type, ret_type) + | _, Arrow (_, ((Aerasable | Aimplicit) as ak), (_l,v), arg_type, ret_type) (* Don't instantiate after the last explicit arg: the rest is done, * when needed in infer_and_check (via instantiate_implicit). *) when not (sargs = [] && SMap.is_empty pending) @@ -1544,7 +1549,7 @@ let sform_immediate ctx loc sargs ot =
let sform_identifier ctx loc sargs ot = match sargs with - | [Symbol (l,name)] + | [Symbol (l, name)] when String.length name >= 1 && String.get name 0 == '#' -> if String.length name > 2 && String.get name 1 == '#' then let name = string_sub name 2 (String.length name) in @@ -1606,15 +1611,19 @@ let sform_identifier ctx loc sargs ot = match ot with Some _ -> Checked | None -> Lazy)
(* Normal identifier. *) - | [Symbol _] -> elab_varref ctx (loc, "") + | [Symbol (_, name)] + -> elab_varref ctx (loc, name)
- | [se] - -> (sexp_error (sexp_location se) ("Non-symbol passed to ##typer-identifier"); + + | [_se] + -> (sexp_error (sexp_location loc) ("Non-symbol passed to ##typer-identifier"); sform_dummy_ret ctx loc)
| _ -> (sexp_error (sexp_location loc) ("Too many args to ##typer-identifier"); - sform_dummy_ret ctx loc) + print_lexp_ctx (ectx_to_lctx ctx); + raise (Log.Internal_error "ERROR !!!!!!!!!!!!!!!!!!!!!!!! ERROR !!!!!!!!!!!!!!!!!!!!!!!!!!! ERROR"); + (*sform_dummy_ret ctx loc*))
let rec sform_lambda kind ctx loc sargs ot = match sargs with @@ -1631,18 +1640,18 @@ let rec sform_lambda kind ctx loc sargs ot = | _ -> None in
let mklam lt1 olt2 = - let nctx = ectx_extend ctx (loc, None) Variable lt1 in + let nctx = ectx_extend ctx arg Variable lt1 in let olt2 = match olt2 with | None -> None (* Apply a "dummy" substitution which replace #0 with #0 * in order to account for the fact that `arg` and `v` * might not be the same name! *) | Some lt2 - -> Some (srename (loc, None) lt2) in + -> Some (srename arg lt2) in let (lbody, alt) = elaborate nctx sbody olt2 in - (mkLambda (loc, kind, (loc, None), lt1, lbody), + (mkLambda (loc, kind, arg, lt1, lbody), match alt with - | Inferred lt2 -> Inferred (mkArrow (loc, kind, (loc, None), lt1, lt2)) + | Inferred lt2 -> Inferred (mkArrow (loc, kind, arg, lt1, lt2)) | _ -> alt) in
(match ot with @@ -1680,7 +1689,7 @@ let rec sform_lambda kind ctx loc sargs ot = | _ -> alt)
| _lt - -> let (lt1, lt2) = unify_with_arrow ctx loc lp kind (loc, None) olt1 + -> let (lt1, lt2) = unify_with_arrow ctx loc lp kind arg olt1 in mklam lt1 (Some lt2) )
| _
===================================== src/env.ml ===================================== @@ -42,7 +42,8 @@ module L = Lexp module BI = Z (* Was Big_int *) module DB = Debruijn
-let dloc = dummy_sinfo +let dloc = Util.dummy_location +let dsinfo = dummy_sinfo
let fatal ?print_action ?loc fmt = Log.log_fatal ~section:"ENV" ?print_action ?loc fmt @@ -120,7 +121,7 @@ let value_location (vtp: value_type) = | Vcons ((loc, _), _) -> loc | Closure (_, lxp, _) -> elexp_location lxp (* location info was lost or never existed *) - | _ -> (sexp_location dloc) + | _ -> dloc
let rec value_name v = match v with
===================================== src/eval.ml ===================================== @@ -50,7 +50,9 @@ module Prelexer = Prelexer (* prelex_string *)
type eval_debug_info = elexp list * elexp list
-let dloc = dummy_sinfo +let dloc = dummy_location +let dsinfo = dummy_sinfo + let global_eval_trace = ref ([], []) let global_eval_ctx = ref make_runtime_ctx (* let eval_max_recursion_depth = ref 23000 *) @@ -128,11 +130,11 @@ let trace_elexp (elexp : elexp) : string =
(* FIXME: We're not using predef here. This will break if we change * the definition of `Bool` in builtins.typer. *) -let ttrue = Vcons (((sexp_location dloc), "true"), []) -let tfalse = Vcons ((sexp_location dloc, "false"), []) +let ttrue = Vcons ((dloc, "true"), []) +let tfalse = Vcons ((dloc, "false"), []) let o2v_bool b = if b then ttrue else tfalse
-let tunit = Vcons ((sexp_location dloc, "unit"), []) +let tunit = Vcons ((dloc, "unit"), [])
(* I'm using a ref because I think register_builtin_functions get called after the default_ctx is created in elab. @@ -537,7 +539,7 @@ and eval_call loc unef i f args = let rec buildbody n = if n > 0 then Lambda (vdummy, buildbody (n - 1)) - else Call (Builtin ((sexp_location dloc), name), buildargs (arity - 1)) in + else Call (Builtin (dloc, name), buildargs (arity - 1)) in Closure (vdummy, buildbody (arity - nargs - 1), buildctx args Myers.nil) @@ -750,8 +752,8 @@ let sys_exit loc _depth args_val = match args_val with let y_operator loc _depth args = match args with | [f] -> let yf_ref = ref Vundefined in - let fname = (dloc, Some "f") in - let yfname = (dloc, Some "yf") in + let fname = (dsinfo, Some "f") in + let yfname = (dsinfo, Some "yf") in let yf = Closure(vdummy, Call (Var (fname, 1), [Var (yfname, 2); @@ -785,7 +787,7 @@ let gensym = let count = ref 0 in (fun loc _depth args_val -> match args_val with | [_v] -> Vcommand (fun () -> ( count := ((!count) + 1); - Vsexp (Symbol ((sexp_location dloc),(" %gensym% no "^(string_of_int (!count))^" "))))) + Vsexp (Symbol (dloc,(" %gensym% no "^(string_of_int (!count))^" "))))) | _ -> error loc "gensym takes a Unit as argument")
let getenv loc _depth args_val = match args_val with @@ -803,7 +805,7 @@ let constructor_p name ectx = (* Use `lexp_whnf` so that `name` can be indirectly * defined as a constructor * (e.g. as in `let foo = cons in case foo x xs | ...` *) - match OL.lexp'_whnf (mkVar ((dloc, Some name), idx) ) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dsinfo, Some name), idx) ) (ectx_to_lctx ectx) with | Cons _ -> true (* It's indeed a constructor! *) | _ -> false with Senv_Lookup_Fail _ -> false @@ -817,7 +819,7 @@ let erasable_p name nth ectx = else false | _ -> false in try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dloc, Some name), idx) ) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dsinfo, Some name), idx) ) (ectx_to_lctx ectx) with | Cons (e, _) when is_var e -> (match (env_lookup_expr ectx (get_var e)) with | Some i when is_inductive i @@ -838,7 +840,7 @@ let erasable_p2 t name ectx = args) | _ -> false in try let idx = senv_lookup t ectx in - match OL.lexp'_whnf (mkVar ((dloc, Some t), idx) ) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dsinfo, Some t), idx) ) (ectx_to_lctx ectx) with | Cons (e, _) when is_var e -> (match (env_lookup_expr ectx (get_var e)) with | Some i when is_inductive i @@ -856,7 +858,7 @@ let nth_ctor_arg name nth ectx = | exception (Failure _) -> "_" ) | _ -> "_" in try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dloc, Some name), idx) ) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dsinfo, Some name), idx) ) (ectx_to_lctx ectx) with | Cons (e, _) when is_var e -> (match (env_lookup_expr ectx (get_var e)) with | Some i when is_inductive i @@ -877,7 +879,7 @@ let ctor_arg_pos name arg ectx = | Some n -> n ) | _ -> (-1) in try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dloc, Some name), idx) ) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dsinfo, Some name), idx) ) (ectx_to_lctx ectx) with | Cons (e, _) when is_var e -> (match (env_lookup_expr ectx (get_var e)) with | Some i when is_inductive i
===================================== src/lexp.ml ===================================== @@ -173,13 +173,6 @@ let metavar_lookup (id : meta_id) : metavar_info -> Log.log_fatal ~section:"LEXP" "metavar lookup failure!"
- - - - - - - (********************** Hash-consing **********************)
(** Hash-consing test ** @@ -477,7 +470,7 @@ let ssink = S.sink (fun l i -> mkVar (l, i) )
(* Apply a "dummy" substitution which replace #0 with #0 * in order to account for changes to a variable's name. - * This should probably `````be made into a no-op, but only after we get rid + * This should probably be made into a no-op, but only after we get rid * of the check in DB.lookup that a `Var` has the same name as the * one stored in the lctx! * Using DeBruijn *should* make α-renaming unnecessary @@ -519,23 +512,23 @@ let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5)))
let rec lexp_sinfo e = match lexp_lexp' e with - | Sort (si,_) -> si + | Sort (s,_) -> s | SortLevel (SLsucc e) -> lexp_sinfo e | SortLevel (SLlub (e, _)) -> lexp_sinfo e | SortLevel SLz -> dummy_sinfo | Imm s -> s - | Var ((_si,_),_) -> dummy_sinfo - | Builtin ((_si, _), _) -> dummy_sinfo - | Let (si,_,_) -> si - | Arrow (si,_,_,_,_) -> si - | Lambda (_,_,(_si,_),_,_) -> dummy_sinfo - | Call (_,f,_) -> lexp_sinfo f - | Inductive (si,_,_,_) -> si - | Cons (_,(_si,_)) -> dummy_sinfo - | Case (si,_,_,_,_) -> si + | Var ((_s,_),_) -> dummy_sinfo + | Builtin ((_s, _), _) -> dummy_sinfo + | Let (s,_,_) -> s + | Arrow (s,_,_,_,_) -> s + | Lambda (_,_,(_s,_),_,_) -> dummy_sinfo + | Call (_,s,_) -> lexp_sinfo s + | Inductive (s,_,_,_) -> s + | Cons (_,(_s,_)) -> dummy_sinfo + | Case (s,_,_,_,_) -> s | Susp (e, _) -> lexp_sinfo e (* | Susp (_, e) -> lexp_location e *) - | Metavar (_,_,(_l,_)) -> dummy_sinfo + | Metavar (_,_,(_s,_)) -> dummy_sinfo
let lexp_location e =
===================================== src/opslexp.ml ===================================== @@ -688,7 +688,7 @@ and check'' erased ctx e = -> let ft = check erased ctx f in List.fold_left (fun ft (ak, arg) - -> let at = check (if ak = P.Aerasable then DB.set_empty else erased) (*(if ak = P.Aerasable then DB.set_empty else erased)*) + -> let at = check (if ak = P.Aerasable then DB.set_empty else erased) ctx arg in match lexp'_whnf ft ctx with | Arrow (_l, ak', _v, t1, t2) @@ -701,6 +701,7 @@ and check'' erased ctx e = "Calling a non functin (type = %s)!" (lexp_string ft); ft) ft args + | Inductive (l, _label, args, cases) -> let rec arg_loop ctx erased args = match args with @@ -1027,7 +1028,7 @@ and get_type ctx e = match sort_compose ctx nctx l ak k1 k2 with | SortResult k -> k | _ -> mkSort (l, StypeOmega) ) - | Lambda (l, ak, ((_,_) as v), t, e) + | Lambda (l, ak, v, t, e) -> (mkArrow (l, ak, v, t, get_type (DB.lctx_extend ctx v Variable t) e) )
===================================== tests/env_test.ml ===================================== @@ -41,11 +41,11 @@ let _ = (add_test "ENV" "Set Variables" (fun () -> if 10 <= (!global_verbose_lvl) then (
let var = [ - ((dloc, Some "a"), DB.type_int, (make_val "a")); - ((dloc, Some "b"), DB.type_int, (make_val "b")); - ((dloc, Some "c"), DB.type_int, (make_val "c")); - ((dloc, Some "d"), DB.type_int, (make_val "d")); - ((dloc, Some "e"), DB.type_int, (make_val "e")); + ((dsinfo, Some "a"), DB.type_int, (make_val "a")); + ((dsinfo, Some "b"), DB.type_int, (make_val "b")); + ((dsinfo, Some "c"), DB.type_int, (make_val "c")); + ((dsinfo, Some "d"), DB.type_int, (make_val "d")); + ((dsinfo, Some "e"), DB.type_int, (make_val "e")); ] in
let n = (List.length var) - 1 in
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b97ae370138cd9240b840c955894632e04...