Typer Avril 2022

typer@iro.umontreal.ca

2 participants
6 discussions

[Git][monnier/typer][minimal-server] -
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 30 Avr '22

30 Avr '22

Soilihi BEN SOILIHI BOINA pushed to branch minimal-server at Stefan / Typer Commits: d659bbe9 by Soilih at 2022-04-30T18:26:49-04:00 - - - - - - 1 changed file: - src/typer_lsp_server.ml Changes: ===================================== src/typer_lsp_server.ml ===================================== @@ -39,13 +39,12 @@ open Log open Util -type list_in_list = (vname * Lexp.lexp * Lexp.ltype) list list +type syntax_tree = (vname * Lexp.lexp * Lexp.ltype) list list -type syntax_tree = (list_in_list * Debruijn.elab_context) +type syntax_tree_elab_ctx = (syntax_tree * Debruijn.elab_context) -type state_after_processing = (log_entry list * - (syntax_tree option) * ((int * int) option ref) - ) +type document_state = (log_entry list * (syntax_tree_elab_ctx option) + * ((int * int) option ref)) (* @@ -179,21 +178,21 @@ let construct_log_exec str s : Log.log_entry list = (*compile a string and return the logs and ast*) -let readstring (str:string) = +let compile_string (str:string) = Log.clear_log () ; let ectx = Elab.default_ectx in match Elab.lexp_decl_str str ectx with - | (ast:syntax_tree) -> (!Log.typer_log, Some ast, ref None) + | (ast:syntax_tree_elab_ctx) -> (!Log.typer_log, Some ast, ref None) | exception Internal_error msg -> (construct_log_exec str msg, None, ref None) | exception Stop_compilation msg -> (construct_log_exec str msg, None, ref None) | exception User_error msg -> (construct_log_exec str msg, None, ref None) -let process_some_input_file (_file_contents : string) : state_after_processing = - readstring _file_contents +let process_some_input_file (_file_contents : string) : document_state = + compile_string _file_contents (*Return the diagnostics of a document state *) -let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list = +let diagnostics (_state : document_state) : Lsp.Types.Diagnostic.t list = let (log, _, _) = _state in let log_tab = log_entry_to_list log in List.map (fun x -> @@ -212,8 +211,8 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list diagnostic ) log_tab -let trans_list_in_list_to_let (lst: list_in_list) : Lexp.lexp = - let rec foo (lst: list_in_list) = +let trans_list_in_list_to_let (lst: syntax_tree) : Lexp.lexp = + let rec foo (lst: syntax_tree) = match lst with | [] -> Lexp.impossible | hd::tl -> let rec foo_in_foo (ls : (vname * Lexp.lexp * Lexp.lexp) list) = @@ -229,9 +228,9 @@ in foo lst (*Update the context of a list_list and returns the updated context with the list all in a list *) -let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list = +let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list = - let rec foo (ctx: Debruijn.lexp_context) (liste : list_in_list ) (list_ret: (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list) = + let rec foo (ctx: Debruijn.lexp_context) (liste : syntax_tree ) (list_ret: (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list) = match liste with | [] -> list_ret | hd::tl -> let lctx = Debruijn.lctx_extend_rec ctx hd in @@ -247,7 +246,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D (* Return a lexp if the cursor is between his start and end position *) - let pos_in_lexp_interval (ctx: Debruijn.lexp_context) (lst: list_in_list) (cursor:Source.Location.t) = + let pos_in_lexp_interval (ctx: Debruijn.lexp_context) (lst: syntax_tree) (cursor:Source.Location.t) = let lstr = update_the_context ctx lst in @@ -266,7 +265,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D in foo lstr cursor (* Find the nearest lexp to the cursor *) - let find_the_nearest_lexp (ctx: Debruijn.lexp_context) (lst:list_in_list) (cursor:Source.Location.t) = + let find_the_nearest_lexp (ctx: Debruijn.lexp_context) (lst:syntax_tree) (cursor:Source.Location.t) = let lstr = update_the_context ctx lst in @@ -317,13 +316,13 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D (* Find the lexp the cursor on or the nearest one *) - let lexp_search (ctx: Debruijn.lexp_context) (lst:list_in_list) (cursor:Source.Location.t) = + let lexp_search (ctx: Debruijn.lexp_context) (lst:syntax_tree) (cursor:Source.Location.t) = try pos_in_lexp_interval ctx lst cursor with exn -> find_the_nearest_lexp ctx lst cursor (* If lexp_search didn't find something, give the last context and a dummy lexp *) - let lexp_search_deeper (ctx: Debruijn.lexp_context) (lst:list_in_list) (cursor:Source.Location.t) = + let lexp_search_deeper (ctx: Debruijn.lexp_context) (lst:syntax_tree) (cursor:Source.Location.t) = let lstr = update_the_context ctx lst in let lstr_rev = List.rev lstr in let (last_ctx,_) = List.hd lstr_rev in @@ -595,9 +594,6 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D | MVal e -> let e = Lexp.push_susp e s in browse_lexp ctx e cursor lst_in | MVar (_, t, _) -> (ctx, None, Lexp.push_susp t s, None, location, lst_in)) - - - (*====================================Lexp parcourir===================================*) @@ -1052,7 +1048,7 @@ class lsp_server = inherit Linol_lwt.Jsonrpc2.server as super (* one env per document *) - val buffers: (Lsp.Types.DocumentUri.t, state_after_processing) Hashtbl.t + val buffers: (Lsp.Types.DocumentUri.t, document_state) Hashtbl.t = Hashtbl.create 96 (* We define here a helper method that will: - process a document @@ -1138,7 +1134,7 @@ class lsp_server = method! on_req_definition ~notify_back ~id ~uri ~pos _st = match Hashtbl.find buffers uri with - | state_after_processing -> let (_,ast,cur) = state_after_processing in + | document_state -> let (_,ast,cur) = document_state in cur := Some (pos.line,pos.character); let (list_list, _) = Option.get ast in let typer_loc = typer_pos_of_lsp_pos pos in @@ -1172,7 +1168,7 @@ class lsp_server = method! on_req_hover ~notify_back:_ ~id:_ ~uri ~pos _ = match Hashtbl.find buffers uri with - | state_after_processing -> let (_,ast,_) = state_after_processing in + | document_state -> let (_,ast,_) = document_state in let (list_list, _) = Option.get ast in let typer_loc = typer_pos_of_lsp_pos pos in let typer_loc' = { @@ -1180,16 +1176,17 @@ class lsp_server = end_line = typer_loc.start_line + 1 } in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + (* let lexp = trans_list_in_list_to_let list_list in let (l_ctx,_,l_type,_,location,_) = browse_lexp ctx lexp typer_loc' [] in - (* + *) let (lctx,vx) = lexp_search ctx list_list typer_loc' in let ((lvn,_),lexp,ltyp) = vx in let (l_ctx_r,_,_,_,_,_) as ret = browse_lexp lctx lexp typer_loc' [] in let ret' = (l_ctx_r,None,ltyp,None,lvn,[]) in let (l_ctx,_,l_type,_,location,_) = browse_list_lexp [ret;ret'] typer_loc in - *) + let range = lsp_range_of_loc location in let range' = Lsp.Types.Range.{ start = { range.start with line = range.start.line - 1 } ; @@ -1209,7 +1206,7 @@ class lsp_server = method! on_req_completion ~notify_back ~id ~uri ~pos ~ctx doc_state = match Hashtbl.find buffers uri with - | state_after_processing -> let (_,ast,cur) = state_after_processing in + | document_state -> let (_,ast,cur) = document_state in cur := Some (pos.line,pos.character); let (list_list, _) = Option.get ast in let typer_loc = typer_pos_of_lsp_pos pos in @@ -1276,7 +1273,7 @@ class lsp_server = match Hashtbl.find buffers uri with - | state_after_processing -> let (_,ast, cur) = state_after_processing in + | document_state -> let (_,ast, cur) = document_state in let (list_list, _) = Option.get ast in let typer_loc = pos_of_tuple (Option.get !cur) in let typer_loc' = { @@ -1302,7 +1299,7 @@ class lsp_server = | TextDocumentHighlight params -> ( match Hashtbl.find buffers params.textDocument.uri with - | state_after_processing -> let (_,ast,cur) = state_after_processing in + | document_state -> let (_,ast,cur) = document_state in cur := Some (params.position.line,params.position.character); let (list_list, _) = Option.get ast in let typer_loc = typer_pos_of_lsp_pos params.position in @@ -1325,7 +1322,7 @@ class lsp_server = | TextDocumentReferences params -> ( match Hashtbl.find buffers params.textDocument.uri with - | state_after_processing -> let (_,ast,cur) = state_after_processing in + | document_state -> let (_,ast,cur) = document_state in cur := Some (params.position.line,params.position.character); let (list_list, _) = Option.get ast in let typer_loc = typer_pos_of_lsp_pos params.position in @@ -1357,7 +1354,7 @@ let afficher_lst code filename = let ch = open_in code in let content = really_input_string ch (in_channel_length ch) in close_in ch; - let (_,ast,_) = readstring content in + let (_,ast,_) = compile_string content in let (list_list, _) = Option.get ast in List.iteri (fun i x -> let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 filename in @@ -1380,7 +1377,7 @@ let afficher_lst code filename = ) list_list let testerBread cursor str = - let (_,ast,_) = readstring str in + let (_,ast,_) = compile_string str in let (list_list, _) = Option.get ast in let typer_loc = pos_of_tuple cursor in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in View it on GitLab: https://gitlab.com/monnier/typer/-/commit/d659bbe972bedbbecc0309a90bce781a4… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/d659bbe972bedbbecc0309a90bce781a4… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][track-sexp-lexp] String.sub
by Ismaila FALL (＠Fallismaila) 28 Avr '22

28 Avr '22

Ismaila FALL pushed to branch track-sexp-lexp at Stefan / Typer Commits: 62b305cd by “falismai(a)iro.umontreal.xn--ca-02t at 2022-04-27T15:48:06+00:00 String.sub - - - - - 17 changed files: - − .idea/.gitignore - − .idea/misc.xml - − .idea/modules.xml - − .idea/typer.iml - − .idea/vcs.xml - − .vscode/settings.json - debug_util.ml - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/positivity.ml - src/unification.ml - tests/unify_test.ml Changes: ===================================== .idea/.gitignore deleted ===================================== @@ -1,8 +0,0 @@ -# Default ignored files -/shelf/ -/workspace.xml -# Editor-based HTTP Client requests -/httpRequests/ -# Datasource local storage ignored files -/dataSources/ -/dataSources.local.xml ===================================== .idea/misc.xml deleted ===================================== @@ -1,8 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<project version="4"> - <component name="SwUserDefinedSpecifications"> - <option name="specTypeByUrl"> - <map /> - </option> - </component> -</project> \ No newline at end of file ===================================== .idea/modules.xml deleted ===================================== @@ -1,8 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<project version="4"> - <component name="ProjectModuleManager"> - <modules> - <module fileurl="file://$PROJECT_DIR$/.idea/typer.iml" filepath="$PROJECT_DIR$/.idea/typer.iml" /> - </modules> - </component> -</project> \ No newline at end of file ===================================== .idea/typer.iml deleted ===================================== @@ -1,9 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<module type="JAVA_MODULE" version="4"> - <component name="NewModuleRootManager" inherit-compiler-output="true"> - <exclude-output /> - <content url="file://$MODULE_DIR$" /> - <orderEntry type="inheritedJdk" /> - <orderEntry type="sourceFolder" forTests="false" /> - </component> -</module> \ No newline at end of file ===================================== .idea/vcs.xml deleted ===================================== @@ -1,6 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<project version="4"> - <component name="VcsDirectoryMappings"> - <mapping directory="" vcs="Git" /> - </component> -</project> \ No newline at end of file ===================================== .vscode/settings.json deleted ===================================== @@ -1,6 +0,0 @@ -{ - "ocaml.sandbox": { - "kind": "opam", - "switch": "default" - } -} \ No newline at end of file ===================================== debug_util.ml ===================================== @@ -58,8 +58,8 @@ open Builtin open Debruijn open Env -let dloc = dummy_sinfo -let dummy_decl = Imm(String(sexp_location(dloc), "Dummy")) +let dsinfo = dummy_sinfo +let dummy_decl = Imm (String (dsinfo, "Dummy")) let discard _v = () @@ -306,7 +306,7 @@ let main () = let main = (senv_lookup "main" nctx) in (* get main body *) - let body = (get_rte_variable (dloc, Some "main") main rctx) in + let body = (get_rte_variable (dsinfo, Some "main") main rctx) in (* eval main *) print_eval_result 1 body ===================================== src/builtin.ml ===================================== @@ -53,11 +53,13 @@ * * ---------------------------------------------------------------------------*) -(* open Pexp *) (* arg_kind *) +(* open Pexp + open Sexp + *) (* arg_kind *) module OL = Opslexp open Lexp -open Sexp + module DB = Debruijn module E = Env @@ -98,10 +100,11 @@ let set_predef name lexp = predef_map := SMap.add name lexp (!predef_map) (* Builtin types *) -let dloc = DB.dloc +let dloc = DB.dloc +let dsinfo = DB.dsinfo -let op_binary t = mkArrow (Anormal, (dloc, None), t, dloc, - mkArrow (Anormal, (dloc, None), t, dloc, t) ) +let op_binary t = mkArrow (dsinfo, Anormal, (dsinfo, None), t, + mkArrow (dsinfo, Anormal, (dsinfo, None), t, t) ) let o2l_bool ctx b = get_predef (if b then "true" else "false") ctx @@ -110,8 +113,8 @@ let o2v_list lst = (* FIXME: We're not using predef here. This will break if we change * the definition of `List` in builtins.typer. *) List.fold_left (fun tail elem - -> E.Vcons (((sexp_location dloc), "cons"), [E.Vsexp (elem); tail])) - (E.Vcons (((sexp_location dloc), "nil"), [])) + -> E.Vcons ((dloc, "cons"), [E.Vsexp (elem); tail])) + (E.Vcons ((dloc, "nil"), [])) (List.rev lst) @@ -141,7 +144,7 @@ let add_builtin_cst (name : string) (e : lexp) lmap := SMap.add name (e, t) map let new_builtin_type name kind = - let t = mkBuiltin (((sexp_location dloc), name), kind) in + let t = mkBuiltin ((dloc, name), kind) in add_builtin_cst name t; t @@ -160,7 +163,7 @@ let register_builtin_csts () = add_builtin_cst "Eq.refl" DB.eq_refl let type_arrow_0 = - mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0) + mkArrow (dsinfo, Anormal, (dsinfo, None), DB.type0, DB.type0) let register_builtin_types () = let _ = new_builtin_type "Sexp" DB.type0 in ===================================== src/debruijn.ml ===================================== @@ -83,48 +83,51 @@ let fatal ?print_action ?loc fmt = (* Type definitions * ---------------------------------- *) -let dloc = dummy_sinfo -let type_level_sort = mkSort (dloc, StypeLevel) -let sort_omega = mkSort (dloc, StypeOmega) -let type_level = mkBuiltin ((sexp_location dloc, "TypeLevel"), type_level_sort) +let dloc = dummy_location +let dsinfo = dummy_sinfo + + +let type_level_sort = mkSort (dsinfo, StypeLevel) +let sort_omega = mkSort (dsinfo, StypeOmega) +let type_level = mkBuiltin ((dloc, "TypeLevel"), type_level_sort) let level0 = mkSortLevel SLz let level1 = mkSortLevel (mkSLsucc level0) let level2 = mkSortLevel (mkSLsucc level1) -let type0 = mkSort (dloc, Stype level0) -let type1 = mkSort (dloc, Stype level1) -let type2 = mkSort (dloc, Stype level2) -let type_int = mkBuiltin ((sexp_location dloc, "Int"), type0) -let type_integer = mkBuiltin ((sexp_location dloc, "Integer"), type0) -let type_float = mkBuiltin ((sexp_location dloc, "Float"), type0) -let type_string = mkBuiltin ((sexp_location dloc, "String"), type0) -let type_elabctx = mkBuiltin ((sexp_location dloc, "Elab_Context"), type0) +let type0 = mkSort (dsinfo, Stype level0) +let type1 = mkSort (dsinfo, Stype level1) +let type2 = mkSort (dsinfo, Stype level2) +let type_int = mkBuiltin ((dloc, "Int"), type0) +let type_integer = mkBuiltin ((dloc, "Integer"), type0) +let type_float = mkBuiltin ((dloc, "Float"), type0) +let type_string = mkBuiltin ((dloc, "String"), type0) +let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0) let type_eq_type = - let lv = (dloc, Some "l") in - let tv = (dloc, Some "t") in - mkArrow (Aerasable, lv, - type_level, dloc, - mkArrow (Aerasable, tv, - mkSort (dloc, Stype (mkVar (lv, 0))) , dloc, - mkArrow (Anormal, (dloc, None), - mkVar (tv, 0), dloc, - mkArrow (Anormal, (dloc, None), - mkVar (tv, 1) , dloc, - mkSort (dloc, Stype (mkVar (lv, 3))))))) - -let type_eq = mkBuiltin ((sexp_location dloc, "Eq"), type_eq_type) + let lv = (dsinfo, Some "l") in + let tv = (dsinfo, Some "t") in + mkArrow (dsinfo ,Aerasable, lv, + type_level, + mkArrow (dsinfo, Aerasable, tv, + mkSort (dsinfo, Stype (mkVar (lv, 0))), + mkArrow (dsinfo, Anormal, (dsinfo, None), + mkVar (tv, 0), + mkArrow (dsinfo, Anormal, (dsinfo, None), + mkVar (tv, 1) , + mkSort (dsinfo, Stype (mkVar (lv, 3))))))) + +let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) let eq_refl = - let lv = (dloc, Some "l") in - let tv = (dloc, Some "t") in - let xv = (dloc, Some "x") in - mkBuiltin ((sexp_location dloc, "Eq.refl"), - mkArrow (Aerasable, lv, - type_level, dloc, - mkArrow (Aerasable, tv, - mkSort (dloc, Stype (mkVar (lv, 0))), dloc, - mkArrow (Aerasable, xv, - mkVar (tv, 0), dloc, - mkCall (type_eq, + let lv = (dsinfo, Some "l") in + let tv = (dsinfo, Some "t") in + let xv = (dsinfo, Some "x") in + mkBuiltin ((dloc, "Eq.refl"), + mkArrow (dsinfo, Aerasable, lv, + type_level, + mkArrow (dsinfo, Aerasable, tv, + mkSort (dsinfo, Stype (mkVar (lv, 0))), + mkArrow (dsinfo, Aerasable, xv, + mkVar (tv, 0), + mkCall (dsinfo, type_eq, [Aerasable, mkVar (lv, 2); Aerasable, mkVar (tv, 1); Anormal, mkVar (xv, 0); @@ -197,9 +200,9 @@ let senv_lookup (name: string) (ctx: elab_context): int = else names) map [] in - if ((String.sub name 0 1) = "_" || - (String.sub name ((String.length name) - 1) 1) = "_") && - ((String.length name) > 1) then + if ((String.length name) > 1) && + ((String.sub name 0 1) = "_" || + (String.sub name ((String.length name) - 1) 1) = "_") then search r else [] in ===================================== src/elab.ml ===================================== @@ -62,8 +62,9 @@ module EL = Elexp open Printf -(* dummies *) -let dloc = dummy_sinfo +(* dummies +* let dsinfo = dummy_sinfo +*) let parsing_internals = ref false let btl_folder = @@ -111,7 +112,7 @@ let special_forms : special_forms_map ref = ref SMap.empty let type_special_form = BI.new_builtin_type "Special-Form" type0 let add_special_form (name, func) = - BI.add_builtin_cst name (mkBuiltin (((sexp_location dloc), name) , type_special_form)); + BI.add_builtin_cst name (mkBuiltin ((dloc, name) , type_special_form)); special_forms := SMap.add name func (!special_forms) let get_special_form name = @@ -439,12 +440,12 @@ let meta_to_var ids (e : lexp) = loop (o' + o) t) :: defs)) defs (len, []) in mkLet (l, ndefs, loop (len + o) e) - | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, loop o t1, l, loop (1 + o) t2) - | Lambda (ak, v, t, e) - -> mkLambda (ak, v, loop o t, loop (1 + o) e) - | Call (f, args) - -> mkCall (loop o f, List.map (fun (ak, e) -> (ak, loop o e)) args) + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, loop o t1, loop (1 + o) t2) + | Lambda (l, ak, v, t, e) + -> mkLambda (l, ak, v, loop o t, loop (1 + o) e) + | Call (l, f, args) + -> mkCall (l, loop o f, List.map (fun (ak, e) -> (ak, loop o e)) args) | Inductive (l, label, args, cases) -> let alen = List.length args in let (_, nargs) @@ -617,12 +618,12 @@ and get_implicit_arg ctx loc oname t = (* Build the list of implicit arguments to instantiate. *) and instantiate_implicit e t ctx = - let rec instantiate t args = + let rec instantiate t args = match OL.lexp'_whnf t (ectx_to_lctx ctx) with - | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) + | Arrow (_, ak , (_, v), t1, t2) -> let arg = get_implicit_arg ctx (lexp_location e) v t1 in instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) - | _ -> (mkCall (e, List.rev args), t) + | _ -> (mkCall (dsinfo, e, List.rev args), t) in instantiate t [] and infer_type pexp ectx var = @@ -658,7 +659,7 @@ and infer_type pexp ectx var = t and lexp_let_decls declss (body: lexp) _ctx = - List.fold_right (fun decls lxp -> mkLet (dloc, decls, lxp)) + List.fold_right (fun decls lxp -> mkLet (dsinfo, decls, lxp)) declss body and unify_with_arrow ctx tloc lxp kind var aty @@ -668,7 +669,7 @@ and unify_with_arrow ctx tloc lxp kind var aty let nctx = ectx_extend ctx var Variable arg in let body = newMetatype (ectx_to_lctx nctx) (ectx_to_scope_level ctx) tloc in let (l, _) = var in - let arrow = mkArrow (kind, var, arg, l, body) in + let arrow = mkArrow (l, kind, var, arg, body) in match Unif.unify arrow lxp (ectx_to_lctx ctx) with | ((_ck, _ctx, t1, t2)::_) -> lexp_error @@ -706,7 +707,7 @@ and unify_or_error lctx lxp ?lxp_name expect actual = and check_inferred ctx e inferred_t t = let (e, inferred_t) = match OL.lexp'_whnf t (ectx_to_lctx ctx) with - | Arrow ((Aerasable | Aimplicit), _, _, _, _) + | Arrow (_, (Aerasable | Aimplicit), _, _, _) -> (e, inferred_t) | _ -> instantiate_implicit e inferred_t ctx in unify_or_error (ectx_to_lctx ctx) e t inferred_t; @@ -750,7 +751,7 @@ and check_case rtype (loc, target, ppatterns) ctx = -> unify_ind it it'; (cs, args) | None -> match OL.lexp'_whnf it' (ectx_to_lctx ctx) with - | Inductive (_, _, fargs, constructors) + | Inductive (l, _, fargs, constructors) -> let (_s, targs) = List.fold_left (fun (s, targs) (ak, name, t) -> let arg = newMetavar @@ -761,12 +762,12 @@ and check_case rtype (loc, target, ppatterns) ctx = (S.identity, []) fargs in let (cs, args) = (constructors, List.rev targs) in - ltarget := check_inferred ctx tlxp tltp (mkCall (it', args)); + ltarget := check_inferred ctx tlxp tltp (mkCall (l, it', args)); it_cs_as := Some (it', cs, args); (cs, args) | _ -> let call_split e = match OL.lexp'_whnf e (ectx_to_lctx ctx) with - | Call (f, args) -> (f, args) + | Call (_, f, args) -> (f, args) | _ -> (e,[]) in let (it, targs) = call_split tltp in unify_ind it it'; @@ -796,7 +797,7 @@ and check_case rtype (loc, target, ppatterns) ctx = let tlxp' = shift_to_extended_ctx nctx tlxp in let tltp' = shift_to_extended_ctx nctx tltp in let tlvl' = shift_to_extended_ctx nctx tlvl in - let eqty = mkCall (DB.type_eq, + let eqty = mkCall (loc, DB.type_eq, [(Aerasable, tlvl'); (* Typelevel *) (Aerasable, tltp'); (* Inductive type *) (Anormal, head_lexp); (* Lexp of the branch head *) @@ -819,7 +820,7 @@ and check_case rtype (loc, target, ppatterns) ctx = let rec inst_args ctx e = let lxp = OL.lexp_whnf e (ectx_to_lctx ctx) in match lexp_lexp' lxp with - | Lambda (Aerasable, v, t, body) + | Lambda (_, Aerasable, v, t, body) -> let arg = newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) v t in let nctx = ctx_extend ctx v Variable t in @@ -890,11 +891,11 @@ and check_case rtype (loc, target, ppatterns) ctx = let nctx, fargs = make_nctx ctx subst pargs cargs SMap.empty [] in let head_lexp_ctor = shift_to_extended_ctx nctx - (mkCall (lctor, List.map (fun (_, a) -> (Aerasable, a)) targs)) in + (mkCall (loc, lctor, List.map (fun (_, a) -> (Aerasable, a)) targs)) in let head_lexp_args = List.mapi (fun i (ak, vname) -> (ak, mkVar (vname, List.length fargs - i - 1))) fargs in - let head_lexp = mkCall (head_lexp_ctor, head_lexp_args) in + let head_lexp = mkCall (loc, head_lexp_ctor, head_lexp_args) in let nctx = ctx_extend_with_eq nctx head_lexp in let rtype' = shift_to_extended_ctx nctx rtype in let lexp = check pexp rtype' nctx in @@ -943,7 +944,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = let rec handle_fun_args largs sargs pending ltp = let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) in match sargs, lexp_lexp' ltp' with - | _, Arrow (ak, (_, Some aname), arg_type, _, ret_type) + | _, Arrow (_, ak, (_, Some aname), arg_type, ret_type) when SMap.mem aname pending -> let sarg = SMap.find aname pending in let larg = check sarg arg_type ctx in @@ -952,7 +953,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = (L.mkSusp ret_type (S.substitute larg)) | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs, - Arrow (ak, _, arg_type, _, ret_type) + Arrow (_, ak, _, arg_type, ret_type) when (aname = "_") (* Explicit-implicit argument. *) -> let larg = check sarg arg_type ctx in @@ -972,7 +973,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = handle_fun_args largs sargs pending ltp (* Aerasable *) - | _, Arrow ((Aerasable | Aimplicit) as ak, (_l,v), arg_type, _, ret_type) + | _, Arrow (_, 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) @@ -996,16 +997,16 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = | sarg :: sargs, _ -> let (arg_type, ret_type) = match lexp_lexp' ltp' with - | Arrow (ak, _, arg_type, _, ret_type) + | Arrow (_, ak, _, arg_type, ret_type) -> assert (ak = Anormal); (arg_type, ret_type) | _ -> unify_with_arrow ctx sarg - ltp' Anormal (dloc, None) None in + ltp' Anormal (sarg, None) None in let larg = check sarg arg_type ctx in handle_fun_args ((Anormal, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg)) in let (largs, ret_type) = handle_fun_args [] sargs SMap.empty ltp in - (mkCall (func, List.rev largs), Inferred ret_type) + (mkCall (loc, func, List.rev largs), Inferred ret_type) (* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx = @@ -1022,11 +1023,11 @@ and lexp_parse_inductive ctors ctx = * things like `fv` and `meta_to_var`. *) let altacc = List.fold_right (fun (ak, n, t) aa - -> mkArrow (ak, n, t, dummy_sinfo, aa)) + -> mkArrow (dsinfo, ak, n, t, aa)) acc impossible in let g = generalize nctx altacc in let altacc' = g (fun _ne vname t l e - -> mkArrow (Aerasable, vname, t, l, e)) + -> mkArrow (l, Aerasable, vname, t, e)) altacc in if altacc' == altacc then acc (* No generalization! *) @@ -1034,7 +1035,7 @@ and lexp_parse_inductive ctors ctx = (* Convert the Lexp back into a list of fields. *) let rec loop e = match lexp_lexp' e with - | Arrow (ak, n, t, _, e) -> (ak, n, t)::(loop e) + | Arrow (_, ak, n, t, e) -> (ak, n, t)::(loop e) | _ -> assert (e = impossible); [] in loop altacc' | (kind, var, exp)::tl @@ -1102,7 +1103,7 @@ and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) let args = [macro; BI.o2v_list sargs] in (* FIXME: Make a proper `Var`. *) - EV.eval_call loc (EL.Var ((DB.dloc, Some "expand_macro"), 0)) ([], []) + EV.eval_call loc (EL.Var ((dsinfo, Some "expand_macro"), 0)) ([], []) macro_expand args (* Print each generated decls *) @@ -1198,7 +1199,7 @@ and infer_and_generalize_type (ctx : elab_context) se name = | _ -> t in let g = generalize nctx (strip_rettype t) in g (fun _ne name t l e - -> mkArrow (Aerasable, name, t, l, e)) + -> mkArrow (l, Aerasable, name, t, e)) t and infer_and_generalize_def (ctx : elab_context) se = @@ -1206,12 +1207,12 @@ and infer_and_generalize_def (ctx : elab_context) se = let (e,t) = infer se nctx in let g = generalize nctx e in let e' = g (fun ne vname t _l e - -> mkLambda ((if ne then Aimplicit else Aerasable), + -> mkLambda (se, (if ne then Aimplicit else Aerasable), vname, t, e)) e in let t' = g (fun ne name t _l e - -> mkArrow ((if ne then Aimplicit else Aerasable), - name, t, se, e)) + -> mkArrow (se, (if ne then Aimplicit else Aerasable), + name, t, e)) t in (e', t') @@ -1518,7 +1519,7 @@ let sform_arrow kind ctx loc sargs _ot = let lt1 = infer_type st1 ctx v in let nctx = ectx_extend ctx v Variable lt1 in let lt2 = infer_type st2 nctx (st2, None) in - (mkArrow (kind, v, lt1, loc, lt2), Lazy) + (mkArrow (loc, kind, v, lt1, lt2), Lazy) | _ -> sexp_error (sexp_location loc) "##_->_ takes two arguments"; sform_dummy_ret ctx loc @@ -1638,9 +1639,9 @@ let rec sform_lambda kind ctx loc sargs ot = | Some lt2 -> Some (srename (loc, None) lt2) in let (lbody, alt) = elaborate nctx sbody olt2 in - (mkLambda (kind, (loc, None), lt1, lbody), + (mkLambda (loc, kind, (loc, None), lt1, lbody), match alt with - | Inferred lt2 -> Inferred (mkArrow (kind, (loc, None), lt1, loc, lt2)) + | Inferred lt2 -> Inferred (mkArrow (loc, kind, (loc, None), lt1, lt2)) | _ -> alt) in (match ot with @@ -1653,7 +1654,7 @@ let rec sform_lambda kind ctx loc sargs ot = | Some t -> let lp = OL.lexp_whnf t (ectx_to_lctx ctx) in match lexp_lexp' lp with - | Arrow (ak2, _, lt1, _, lt2) when ak2 = kind + | Arrow (_, ak2, _, lt1, lt2) when ak2 = kind -> (match olt1 with | None -> () | Some lt1' @@ -1661,7 +1662,7 @@ let rec sform_lambda kind ctx loc sargs ot = ~lxp_name:"parameter" lt1 lt1'); mklam lt1 (Some lt2) - | Arrow (ak2, v, lt1, _, lt2) when kind = Anormal + | Arrow (_, ak2, v, lt1, lt2) when kind = Anormal (* `t` is an implicit arrow and `kind` is Anormal, * so auto-add a corresponding Lambda wrapper! * FIXME: This should be moved to a macro. *) @@ -1672,9 +1673,9 @@ let rec sform_lambda kind ctx loc sargs ot = (* FIXME: Don't go back to sform_lambda, but use an internal * loop to avoid re-computing olt1 each time. *) let (lam, alt) = sform_lambda kind nctx loc sargs (Some lt2) in - (mkLambda (ak2, v, lt1, lam), + (mkLambda (loc, ak2, v, lt1, lam), match alt with - | Inferred lt2' -> Inferred (mkArrow (ak2, v, lt1, loc, lt2')) + | Inferred lt2' -> Inferred (mkArrow (loc, ak2, v, lt1, lt2')) | _ -> alt) | _lt @@ -1890,7 +1891,7 @@ let default_ectx let register_predefs elctx = try List.iter (fun name -> let idx = senv_lookup name elctx in - let v = mkVar ((dloc, Some name), idx) in + let v = mkVar ((dsinfo, Some name), idx) in BI.set_predef name v) BI.predef_names; with Senv_Lookup_Fail _ -> warning "Predef not found"; in @@ -1899,7 +1900,7 @@ let default_ectx let lctx = empty_elab_context in let lctx = SMap.fold (fun key (e, t) ctx -> if String.get key 0 = '-' then ctx - else ctx_define ctx (dloc, Some key) e t) + else ctx_define ctx (dsinfo, Some key) e t) (!BI.lmap) lctx in Heap.register_builtins (); ===================================== src/eval.ml ===================================== @@ -553,7 +553,7 @@ and eval_call loc unef i f args = (* We may call a Vlexp e.g. for "x = Map Int String". * FIXME: The arg will sometimes be a Vlexp but not always, so this is * really just broken! *) - -> Vtype (L.mkCall (e, [(Anormal, mkVar (vdummy, -1) )]) ) + -> Vtype (L.mkCall (dsinfo, e, [(Anormal, mkVar (vdummy, -1) )]) ) | _ -> fatal loc "Trying to call a non-function!\n%s" (trace_value f) and eval_case ctx i loc target pat dflt = @@ -624,18 +624,18 @@ and eval_decls (decls: (vname * elexp) list) (String -> Sexp) -> (Int -> Sexp) -> (Float -> Sexp) -> (List Sexp -> Sexp) -> Sexp *) and sexp_dispatch loc depth args = - let trace_dum = (Var ((loc, None), -1)) in - let eval_call a b = eval_call (sexp_location loc) trace_dum depth a b in + let trace_dum = (Var ((Symbol (loc, ""), None), -1)) in + let eval_call a b = eval_call loc trace_dum depth a b in let sxp, nd, sym, str, it, flt, blk = match args with | [sxp; nd; sym; str; it; flt; blk] -> sxp, nd, sym, str, it, flt, blk - | _ -> error (sexp_location loc) "sexp_dispatch expects 7 arguments" in + | _ -> error loc "sexp_dispatch expects 7 arguments" in let sxp = match sxp with | Vsexp(sxp) -> sxp | _ -> fatal - (sexp_location loc) + loc "sexp_dispatch expects a Sexp as 1st arg\n%s" (trace_value sxp) in @@ -711,17 +711,17 @@ and print_eval_trace trace = let (a, _b) = !global_eval_trace in print_trace " EVAL TRACE " trace a -let io_bind loc depth args_val = - let trace_dum = (Var ((loc, None), -1)) in +let io_bind (loc: location) depth args_val = + let trace_dum = (Var ((Symbol (loc, ""), None), -1)) in match args_val with | [Vcommand cmd; callback] -> (* bind returns another Vcommand *) Vcommand (fun () - -> match eval_call (sexp_location loc) trace_dum depth callback [cmd ()] with + -> match eval_call loc trace_dum depth callback [cmd ()] with | Vcommand cmd -> cmd () - | _ -> error (sexp_location loc) "IO.bind second arg did not return a command") - | _ -> error (sexp_location loc) "Wrong number of args or wrong first arg value in `IO.bind`" + | _ -> error loc "IO.bind second arg did not return a command") + | _ -> error loc "Wrong number of args or wrong first arg value in `IO.bind`" let io_run loc _depth args_val = match args_val with | [Vcommand cmd; v] -> let _ = cmd () in v @@ -1030,7 +1030,7 @@ let register_builtin_functions () = ("Sexp.integer" , make_integer, 1); ("Sexp.float" , make_float, 1); ("Sexp.node" , make_node, 2); - (*("Sexp.dispatch" , sexp_dispatch, 7);*) + ("Sexp.dispatch" , sexp_dispatch, 7); ("TypeLevel.succ" , typelevel_succ, 1); ("TypeLevel.⊔" , typelevel_lub, 2); ("Reader.parse" , reader_parse,2); @@ -1042,7 +1042,7 @@ let register_builtin_functions () = ("Float->String" , float_to_string, 1); ("Int->String" , int_to_string, 1); ("Integer->String", integer_to_string, 1); - (*("IO.bind" , io_bind, 2);*) + ("IO.bind" , io_bind, 2); ("IO.return" , io_return, 1); ("IO.run" , io_run, 2); ("Sys.exit" , sys_exit, 1); ===================================== src/inverse_subst.ml ===================================== @@ -275,13 +275,13 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = :: ndefs)) (s, []) defs in mkLet (l, ndefs, apply_inv_subst e s' ) - | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, apply_inv_subst t1 s , l, + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, apply_inv_subst t1 s , apply_inv_subst t2 (ssink v s) ) - | Lambda (ak, v, t, e) - -> mkLambda (ak, v, apply_inv_subst t s , apply_inv_subst e (ssink v s) ) - | Call (f, args) - -> mkCall (apply_inv_subst f s , + | Lambda (l, ak, v, t, e) + -> mkLambda (l, ak, v, apply_inv_subst t s , apply_inv_subst e (ssink v s) ) + | Call (l, f, args) + -> mkCall (l, apply_inv_subst f s , L.map (fun (ak, arg) -> (ak, apply_inv_subst arg s )) args) | Inductive (l, label, args, cases) -> let (s, nargs) ===================================== src/lexp.ml ===================================== @@ -72,9 +72,9 @@ type ltype = lexp | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) | Let of sinfo * (vname * lexp * ltype) list * lexp - | Arrow of arg_kind * vname * ltype * sinfo * ltype - | Lambda of arg_kind * vname * ltype * lexp - | Call of lexp * (arg_kind * lexp) list (* Curried call. *) + | Arrow of sinfo * arg_kind * vname * ltype * ltype + | Lambda of sinfo * arg_kind * vname * ltype * lexp + | Call of sinfo * lexp * (arg_kind * lexp) list (* Curried call. *) | Inductive of sinfo * label * ((arg_kind * vname * ltype) list) (* formal Args *) * ((arg_kind * vname * ltype) list) SMap.t @@ -219,12 +219,12 @@ let lexp'_hash (lp : lexp') = (U.combine_hash (lexp_hash lp) (lexp_hash lt)))) ds)) (lexp_hash e))) - | Arrow (k, v, t1, l, t2) + | Arrow (l, k, v, t1, t2) -> U.combine_hash 7 (U.combine_hash (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) (U.combine_hash (lexp_hash t1) (U.combine_hash (Hashtbl.hash l) (lexp_hash t2)))) - | Lambda (k, v, t, e) + | Lambda (_l, k, v, t, e) -> U.combine_hash 8 (U.combine_hash (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) (U.combine_hash (lexp_hash t) (lexp_hash e))) @@ -249,7 +249,7 @@ let lexp'_hash (lp : lexp') = | Metavar (id, s, v) -> U.combine_hash 12 (U.combine_hash id (U.combine_hash (Hashtbl.hash s) (Hashtbl.hash v))) - | Call (e, args) + | Call (_l, e, args) -> U.combine_hash 13 (U.combine_hash (lexp_hash e) (U.combine_hashes (List.map (fun e -> let (ak, lp) = e in (U.combine_hash (Hashtbl.hash ak) (lexp_hash lp))) @@ -280,9 +280,9 @@ let hc_eq e1 e2 = (fun (_, e1, t1) (_, e2, t2) -> t1 == t2 && e1 == e2) defs1 defs2 | (Arrow (ak1, _, t11, _, t21), Arrow (ak2, _, t12, _, t22)) -> ak1 = ak2 && t11 == t12 && t21 == t22 - | (Lambda (ak1, _, t1, e1), Lambda (ak2, _, t2, e2)) + | (Lambda (_, ak1, _, t1, e1), Lambda (_, ak2, _, t2, e2)) -> ak1 = ak2 && t1 == t2 && e1 == e2 - | (Call (e1, as1), Call (e2, as2)) + | (Call (_, e1, as1), Call (_, e2, as2)) -> e1 == e2 && List.for_all2 (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && e1 == e2) as1 as2 | (Inductive (_, l1, as1, ctor1), Inductive (_, l2, as2, ctor2)) @@ -321,17 +321,17 @@ let mkSort (l, s) = hc (Sort (l, s)) let mkBuiltin (v, t) = hc (Builtin (v, t)) let mkVar v = hc (Var v) let mkLet (l, ds, e) = hc (Let (l, ds, e)) -let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2)) -let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) +let mkArrow (l, k, v, t1, t2) = hc (Arrow (l, k, v, t1, t2)) +let mkLambda (l, k, v, t, e) = hc (Lambda (l, k, v, t, e)) let mkInductive (l, n, a, cs) = hc (Inductive (l, n, a, cs)) let mkCons (t, n) = hc (Cons (t, n)) let mkCase (l, e, rt, bs, d) = hc (Case (l, e, rt, bs, d)) let mkMetavar (n, s, v) = hc (Metavar (n, s, v)) -let mkCall (f, es) = +let mkCall (l, f, es) = match lexp_lexp' f, es with - | Call (f', es'), _ -> hc (Call (f', es' @ es)) + | Call (l, f', es'), _ -> hc (Call (l, f', es' @ es)) | _, [] -> f - | _ -> hc (Call (f, es)) + | _ -> hc (Call (l, f, es)) let impossible = mkImm Sexp.dummy_epsilon @@ -519,20 +519,20 @@ let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5))) let rec lexp_location e = match lexp_lexp' e with - | Sort (l,_) -> l + | Sort (si,_) -> si | SortLevel (SLsucc e) -> lexp_location e | SortLevel (SLlub (e, _)) -> lexp_location e | SortLevel SLz -> dummy_sinfo | Imm s -> s - | Var ((_l,_),_) -> dummy_sinfo - | Builtin ((_l, _), _) -> dummy_sinfo - | Let (l,_,_) -> l - | Arrow (_,_,_,l,_) -> l - | Lambda (_,(_l,_),_,_) -> dummy_sinfo - | Call (f,_) -> lexp_location f - | Inductive (l,_,_,_) -> l - | Cons (_,(_l,_)) -> dummy_sinfo - | Case (l,_,_,_,_) -> l + | Var ((_si,_),_) -> dummy_sinfo + | Builtin ((_si, _), _) -> dummy_sinfo + | Let (si,_,_) -> si + | Arrow (si,_,_,_,_) -> si + | Lambda (_,_,(_si,_),_,_) -> dummy_sinfo + | Call (_,f,_) -> lexp_location f + | Inductive (si,_,_,_) -> si + | Cons (_,(_si,_)) -> dummy_sinfo + | Case (si,_,_,_,_) -> si | Susp (e, _) -> lexp_location e (* | Susp (_, e) -> lexp_location e *) | Metavar (_,_,(_l,_)) -> dummy_sinfo @@ -562,10 +562,10 @@ let rec push_susp e s = (* Push a suspension one level down. *) | (v, def, ty) :: defs -> (v, mkSusp def s' , mkSusp ty s ) :: loop (ssink v s) defs in mkLet (l, loop s defs, mkSusp e s' ) - | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, mkSusp t1 s , l, mkSusp t2 (ssink v s) ) - | Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s , mkSusp e (ssink v s) ) - | Call (f, args) -> mkCall (mkSusp f s , + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, mkSusp t1 s , mkSusp t2 (ssink v s) ) + | Lambda (l, ak, v, t, e) -> mkLambda (l, ak, v, mkSusp t s , mkSusp e (ssink v s) ) + | Call (l, f, args) -> mkCall (l, mkSusp f s , L.map (fun (ak, arg) -> (ak, mkSusp arg s )) args) | Inductive (l, label, args, cases) -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) @@ -629,10 +629,10 @@ let clean e = (v, clean s' def, clean s ty) :: ndefs)) (s, []) defs in mkLet (l, ndefs, clean s' e) - | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, clean s t1, l, clean (ssink v s) t2) - | Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink v s) e) - | Call (f, args) -> mkCall (clean s f, + | Arrow (l, ak, v, t1, t2) + -> mkArrow (l, ak, v, clean s t1, clean (ssink v s) t2) + | Lambda (l, ak, v, t, e) -> mkLambda (l, ak, v, clean s t, clean (ssink v s) e) + | Call (l, f, args) -> mkCall (l, clean s f, L.map (fun (ak, arg) -> (ak, clean s arg)) args) | Inductive (l, label, args, cases) -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) @@ -686,7 +686,7 @@ let rec lexp_unparse lxp = | Cons (t, (l, name)) -> Node (sdatacons, [lexp_unparse t; Symbol (l, name)]) - | Lambda (kind, vdef, ltp, body) + | Lambda (_loc, kind, vdef, ltp, body) -> let l = lexp_location lxp in let st = lexp_unparse ltp in Node (Symbol (sexp_location l, match kind with @@ -695,7 +695,7 @@ let rec lexp_unparse lxp = | Aerasable -> "lambda_≡>_"), [Node (Symbol (sexp_location l, "_:_"), [Symbol (sname vdef); st]); lexp_unparse body ]) - | Arrow (arg_kind, (l,oname), ltp1, loc, ltp2) + | Arrow (loc, arg_kind, (l,oname), ltp1, ltp2) -> let ut1 = lexp_unparse ltp1 in Node (Symbol (sexp_location loc, match arg_kind with Anormal -> "_->_" | Aimplicit -> "_=>_" @@ -719,7 +719,7 @@ let rec lexp_unparse lxp = [Node (Symbol (U.dummy_location, "_;_"), sdecls); lexp_unparse body ]) - | Call(lxp, largs) -> (* (arg_kind * lexp) list *) + | Call(_loc, lxp, largs) -> (* (arg_kind * lexp) list *) let sargs = List.map (fun (_kind, elem) -> lexp_unparse elem ) largs in Node (lexp_unparse lxp, sargs) @@ -902,10 +902,10 @@ let rec get_precedence expr ctx = | Lambda _ -> lkp "lambda" | Case _ -> lkp "case" | Let _ -> lkp "let" - | Arrow (Anormal, _, _, _, _) -> lkp "->" - | Arrow (Aimplicit, _, _, _, _) -> lkp "=>" - | Arrow (Aerasable, _, _, _, _) -> lkp "≡>" - | Call (exp, _) -> get_precedence exp ctx + | Arrow (_, Anormal, _, _, _) -> lkp "->" + | Arrow (_, Aimplicit, _, _, _) -> lkp "=>" + | Arrow (_, Aerasable, _, _, _) -> lkp "≡>" + | Call (_, exp, _) -> get_precedence exp ctx | Builtin ((_, name), _) when is_binary_op name -> lkp (get_binary_op_name name) | Var ((_, Some name), _) when is_binary_op name -> @@ -1010,15 +1010,15 @@ and lexp_str ctx (exp : lexp) : string = (keyword "let ") ^ decls ^ (keyword " in ") ^ newline ^ (make_indent idt_lvl) ^ (lexp_stri idt_lvl body ) - | Arrow(k, (_, Some name), tp, _loc, expr) -> + | Arrow(_loc, k, (_, Some name), tp, expr) -> "(" ^ name ^ " : " ^ (lexp_str' tp ) ^ ") " ^ (kind_str k) ^ " " ^ (lexp_str' expr ) - | Arrow(k, (_, None), tp, _loc, expr) -> + | Arrow(_loc, k, (_, None), tp, expr) -> "(" ^ (lexp_str' tp ) ^ " " ^ (kind_str k) ^ " " ^ (lexp_str' expr ) ^ ")" - | Lambda(k, (_loc, name), ltype, lbody) -> + | Lambda(_loc, k, (_, name), ltype, lbody) -> let arg = "(" ^ maybename name ^ " : " ^ (lexp_str' ltype ) ^ ")" in (keyword "lambda ") ^ arg ^ " " ^ (kind_str k) ^ newline ^ @@ -1027,7 +1027,7 @@ and lexp_str ctx (exp : lexp) : string = | Cons(t, (_, ctor_name)) -> (keyword "datacons ") ^ (lexp_str' t ) ^ " " ^ ctor_name - | Call(fname, args) -> + | Call(_loc, fname, args) -> let name, idx = get_name fname in let binop_str op (_, lhs) (_, rhs) = "(" ^ (lexp_str' lhs ) ^ op ^ (index idx) ^ " " ^ (lexp_str' rhs ) ^ ")" in @@ -1151,11 +1151,11 @@ let rec eq e1 e2 = | (Let (_, defs1, e1), Let (_, defs2, e2)) -> eq e1 e2 && List.for_all2 (fun (_, e1, t1) (_, e2, t2) -> eq t1 t2 && eq e1 e2 ) defs1 defs2 - | (Arrow (ak1, _, t11, _, t21), Arrow (ak2, _, t12, _, t22)) + | (Arrow (_, ak1, _, t11, t21), Arrow (_, ak2, _, t12, t22)) -> ak1 = ak2 && eq t11 t12 && eq t21 t22 - | (Lambda (ak1, _, t1, e1), Lambda (ak2, _, t2, e2)) + | (Lambda (_, ak1, _, t1, e1), Lambda (_, ak2, _, t2, e2)) -> ak1 = ak2 && eq t1 t2 && eq e1 e2 - | (Call (e1, as1), Call (e2, as2)) + | (Call (_, e1, as1), Call (_, e2, as2)) -> eq e1 e2 && List.for_all2 (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && eq e1 e2 ) as1 as2 | (Inductive (_, l1, as1, ctor1), Inductive (_, l2, as2, ctor2)) ===================================== src/opslexp.ml ===================================== @@ -127,7 +127,7 @@ let rec lctx_to_subst lctx = L.ssink v s | DB.CVfix (defs, lctx) -> let s1 = lctx_to_subst lctx in - let s2 = lexp_defs_subst DB.dloc S.identity + let s2 = lexp_defs_subst DB.dsinfo S.identity (List.rev defs) in L.scompose s2 s1 @@ -177,17 +177,17 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = * things like full normalization (e.g. lexp_conv_p). *) | Some e' -> lexp_whnf_aux e' ctx ) | Susp (e, s) -> lexp_whnf_aux (push_susp e s ) ctx - | Call (e, []) -> lexp_whnf_aux e ctx - | Call (f, (((_, arg)::args) as xs)) -> + | Call (_l, e, []) -> lexp_whnf_aux e ctx + | Call (_l, f, (((_, arg)::args) as xs)) -> (match lexp_lexp' (lexp_whnf_aux f ctx ) with - | Lambda (_, _, _, body) -> + | Lambda (l, _, _, _, body) -> (* Here we apply whnf to the arg eagerly to kind of stay closer * to the idea of call-by-value, although in this context * we can't really make sure we always reduce the arg to a value. *) - lexp_whnf_aux (mkCall (push_susp body (S.substitute (lexp_whnf_aux arg ctx )) , + lexp_whnf_aux (mkCall (l, push_susp body (S.substitute (lexp_whnf_aux arg ctx )) , args) ) ctx - | Call (f', xs1) -> mkCall (f', List.append xs1 xs) + | Call (l, f', xs1) -> mkCall (l, f', List.append xs1 xs) | Builtin ((_, name), _) -> (match SMap.find_opt name (!reducible_builtins) with | Some f -> Option.value ~default:e (f ctx args) @@ -200,7 +200,7 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = let elevel = match lexp'_whnf (get_type ctx etype) ctx with | Sort (_, Stype l) -> l | _ -> Log.internal_error "" in - mkCall (DB.eq_refl, + mkCall (l, DB.eq_refl, [L.Aerasable, elevel; L.Aerasable, etype; L.Aerasable, e]) in @@ -235,7 +235,7 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = mkCase (l, e, rt, branches, default) in (match lexp_lexp' e' with | Cons (it, (_, name)) -> reduce it name [] - | Call (f, aargs) -> + | Call (l, f, aargs) -> (match lexp_lexp' (lexp_whnf_aux f ctx ) with | Cons (it, (_, name)) -> reduce it name aargs | _ -> mkCase (l, e, rt, branches, default) ) @@ -264,7 +264,7 @@ and eq_cast_whnf ctx args = match args with | [_l; _t; _x; _y; (_, p); _f; (_, fx)] -> (match lexp'_whnf p ctx with - | Call (refl, _) when conv_p ctx refl DB.eq_refl + | Call (_l, refl, _) when conv_p ctx refl DB.eq_refl -> Some (lexp_whnf fx ctx) | _ -> None) | _ -> None @@ -354,17 +354,17 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | _ -> false) | (Builtin ((_, s1), _), Builtin ((_, s2), _)) -> s1 = s2 | (Var (_, v1), Var (_, v2)) -> v1 = v2 - | (Arrow (ak1, vd1, t11, _, t12), Arrow (ak2, _vd2, t21, _, t22)) + | (Arrow (_, ak1, vd1, t11, t12), Arrow (_, ak2, _vd2, t21, t22)) -> ak1 == ak2 && conv_p t11 t21 && conv_p' (DB.lexp_ctx_cons ctx vd1 Variable t11) (set_shift vs') t12 (srename vd1 t22) - | (Lambda (ak1, l1, t1, e1), Lambda (ak2, _l2, t2, e2)) + | (Lambda (_, ak1, l1, t1, e1), Lambda (_, ak2, _l2, t2, e2)) -> ak1 == ak2 && (conv_erase || conv_p t1 t2) && conv_p' (DB.lexp_ctx_cons ctx l1 Variable t1) (set_shift vs') e1 e2 - | (Call (f1, args1), Call (f2, args2)) + | (Call (_, f1, args1), Call (_, f2, args2)) -> let conv_arglist_p args1 args2 : bool = List.fold_left2 (fun eqp (ak1,t1) (ak2,t2) @@ -417,7 +417,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = "Target lexp's kind is not a sort"; in (* 1. Get the inductive for the field types *) let it, aargs = match lexp_lexp' etype with - | Call (f, args) -> (f, args) + | Call (_, f, args) -> (f, args) | _ -> (etype, []) in (* 2. Build the substitution for the inductive arguments *) let fargs, ctors = @@ -432,12 +432,12 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let tlxp = mkSusp target subst in let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in - let eqty = mkCall (DB.type_eq, + let eqty = mkCall (DB.dsinfo, DB.type_eq, [(L.Aerasable, tlvl); (* Typelevel *) (L.Aerasable, tltp); (* Inductive type *) (L.Anormal, hlxp); (* Lexp of the branch head *) (L.Anormal, tlxp)]) in (* Target lexp *) - DB.lexp_ctx_cons ctx (DB.dloc, None) Variable eqty in + DB.lexp_ctx_cons ctx (DB.dsinfo, None) Variable eqty in (* The map module doesn't have a function to compare two maps with the key (which is needed to get the field types from the inductive. Instead, we work with the lists of @@ -468,9 +468,9 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let subst = S.shift offset in let eaargs = List.map (fun (_, a) -> (P.Aerasable, a)) aargs in - let ctor = mkSusp (mkCall (mkCons (it, (sexp_location (DB.dloc), l1)) , + let ctor = mkSusp (mkCall (DB.dsinfo, mkCons (it, (DB.dloc, l1)) , eaargs) ) subst in - let hlxp = mkCall (ctor, args) in + let hlxp = mkCall (DB.dsinfo, ctor, args) in let nctx = ctx_extend_with_eq nctx subst hlxp in conv_p' nctx (set_shift_n vs' (offset + 1)) e1 e2 ) (SMap.bindings cases1) (SMap.bindings cases2) @@ -481,7 +481,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | (Some (v1, e1), Some (_v2, e2)) -> let nctx = DB.lctx_extend ctx v1 Variable etype in let subst = S.shift 1 in - let hlxp = mkVar ((DB.dloc, None), 0) in + let hlxp = mkVar ((DB.dsinfo, None), 0) in let nctx = ctx_extend_with_eq nctx subst hlxp in conv_p' nctx (set_shift_n vs' 2) e1 e2 | None, None -> true @@ -663,7 +663,7 @@ and check'' erased ctx e = (List.length defs) defs in mkSusp (check nerased nctx e ) (lexp_defs_subst l S.identity defs) - | Arrow (ak, v, t1, loc, t2) + | Arrow (loc, ak, v, t1, t2) -> (let k1 = check_type erased ctx t1 in let nctx = DB.lexp_ctx_cons ctx v Variable t1 in let k2 = check_type (DB.set_sink 1 erased) nctx t2 in @@ -678,20 +678,20 @@ and check'' erased ctx e = | SortK2NotType -> log_tc_error ~loc:(sexp_location (lexp_location t2)) "Not a proper type"; mkSort (loc, StypeOmega) ) - | Lambda (ak, ((l,_) as v), t, e) + | Lambda (l, ak, ((_,_) as v), t, e) -> (let _k = check_type DB.set_empty ctx t in - mkArrow (ak, v, t, l, + mkArrow (l, ak, v, t, check (dbset_push ak erased) (DB.lctx_extend ctx v Variable t) e ) ) - | Call (f, args) + | Call (_l, f, args) -> 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) ctx arg in match lexp'_whnf ft ctx with - | Arrow (ak', _v, t1, _l, t2) + | Arrow (_l, ak', _v, t1, t2) -> if ak != ak' then log_tc_error ~loc:(sexp_location (lexp_location arg)) "arg kind mismatch"; assert_type ctx arg at t1; @@ -741,7 +741,7 @@ and check'' erased ctx e = mkSort (l, Stype level) | (ak, v, t)::args -> let _k = check_type DB.set_empty ctx t in - mkArrow (ak, v, t, lexp_location t, + mkArrow (lexp_location t, ak, v, t, arg_loop (DB.lctx_extend ctx v Variable t) (dbset_push ak erased) args) in @@ -751,7 +751,7 @@ and check'' erased ctx e = (* FIXME: Check that the return type isn't TypeLevel. *) -> let call_split e = match lexp_lexp' e with - | Call (f, args) -> (f, args) + | Call (_l, f, args) -> (f, args) | _ -> (e,[]) in let etype = lexp_whnf (check erased ctx e ) ctx in (* FIXME save the type in the case lexp instead of recomputing @@ -779,7 +779,7 @@ and check'' erased ctx e = let tlxp = mkSusp e subst in let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in - let eqty = mkCall (DB.type_eq, + let eqty = mkCall (l, DB.type_eq, [(L.Aerasable, tlvl); (* Typelevel *) (L.Aerasable, tltp); (* Inductive type *) (L.Anormal, hlxp); (* Lexp of the branch head *) @@ -800,13 +800,13 @@ and check'' erased ctx e = -> mkctx (dbset_push ak erased) (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s )) (ssink vdef s) - (mkCall (mkSusp hlxp (S.shift 1) , [(ak, mkVar (vdef, 0) )]) ) + (mkCall (l, mkSusp hlxp (S.shift 1) , [(ak, mkVar (vdef, 0) )]) ) vdefs fieldtypes | _ -> log_tc_error ~loc:(sexp_location l) "Wrong number of args to constructor!"; (erased, ctx, hlxp) in let hctor = - mkCall (mkCons (it, ((sexp_location l), name)) , + mkCall (l, mkCons (it, ((sexp_location l), name)) , List.map (fun (_, a) -> (P.Aerasable, a)) aargs) in let (nerased, nctx, hlxp) = mkctx erased ctx s hctor vdefs fieldtypes in @@ -849,16 +849,16 @@ and check'' erased ctx e = let rec fieldargs ftypes = match ftypes with | [] -> let nargs = List.length fieldtypes + List.length fargs in - mkCall (mkSusp t (S.shift nargs) , + mkCall (l, mkSusp t (S.shift nargs) , indtype fargs (nargs - 1)) | (ak, vd, ftype) :: ftypes - -> mkArrow (ak, vd, ftype, lexp_location ftype, + -> mkArrow (lexp_location ftype, ak, vd, ftype, fieldargs ftypes) in let rec buildtype fargs = match fargs with | [] -> fieldargs fieldtypes | (_ak, ((l,_) as vd), atype) :: fargs - -> mkArrow (P.Aerasable, vd, atype, l, + -> mkArrow (l, P.Aerasable, vd, atype, buildtype fargs) in buildtype fargs with @@ -937,9 +937,9 @@ and fv (e : lexp) : (DB.set * mv_set) = o - 1)) (fv e, len) defs in fv_hoist len fvs - | Arrow (_, _, t1, _, t2) -> fv_union (fv t1) (fv_hoist 1 (fv t2)) - | Lambda (_, _, t, e) -> fv_union (fv_erase (fv t)) (fv_hoist 1 (fv e)) - | Call (f, args) + | Arrow (_, _, _, t1, t2) -> fv_union (fv t1) (fv_hoist 1 (fv t2)) + | Lambda (_, _, _, t, e) -> fv_union (fv_erase (fv t)) (fv_hoist 1 (fv e)) + | Call (_, f, args) -> List.fold_left (fun fvs (ak, arg) -> let afvs = fv arg in fv_union fvs @@ -1019,7 +1019,7 @@ and get_type ctx e = -> let nctx = DB.lctx_extend_rec ctx defs in mkSusp (get_type nctx e) (lexp_defs_subst l S.identity defs) - | Arrow (ak, v, t1, l, t2) + | Arrow (l, ak, v, t1, t2) (* FIXME: Use `check` here but silencing errors? *) -> (let k1 = get_type ctx t1 in let nctx = DB.lexp_ctx_cons ctx v Variable t1 in @@ -1027,11 +1027,11 @@ and get_type ctx e = match sort_compose ctx nctx l ak k1 k2 with | SortResult k -> k | _ -> mkSort (l, StypeOmega) ) - | Lambda (ak, ((l,_) as v), t, e) - -> (mkArrow (ak, v, t, l, + | Lambda (l, ak, ((_,_) as v), t, e) + -> (mkArrow (l, ak, v, t, get_type (DB.lctx_extend ctx v Variable t) e) ) - | Call (f, args) + | Call (_l, f, args) -> let ft = get_type ctx f in List.fold_left (fun ft (_ak,arg) @@ -1069,14 +1069,14 @@ and get_type ctx e = cases (mkSortLevel SLz ) in mkSort (l, Stype level) | (ak, v, t)::args - -> mkArrow (ak, v, t, lexp_location t, + -> mkArrow (lexp_location t, ak, v, t, arg_loop args (DB.lctx_extend ctx v Variable t)) in let tct = arg_loop args ctx in tct | Case (_l, _e, ret, _branches, _default) -> ret | Cons (t, (_l, name)) -> (match lexp'_whnf t ctx with - | Inductive (_l, _, fargs, constructors) + | Inductive (l, _, fargs, constructors) -> (try let fieldtypes = SMap.find name constructors in let rec indtype fargs start_index = @@ -1087,16 +1087,16 @@ and get_type ctx e = let rec fieldargs ftypes = match ftypes with | [] -> let nargs = List.length fieldtypes + List.length fargs in - mkCall (mkSusp t (S.shift nargs) , + mkCall (l, mkSusp t (S.shift nargs) , indtype fargs (nargs - 1)) | (ak, vd, ftype) :: ftypes - -> mkArrow (ak, vd, ftype, lexp_location ftype, + -> mkArrow (lexp_location ftype, ak, vd, ftype, fieldargs ftypes) in let rec buildtype fargs = match fargs with | [] -> fieldargs fieldtypes | (_ak, ((l,_) as vd), atype) :: fargs - -> mkArrow (P.Aerasable, vd, atype, l, + -> mkArrow (l, P.Aerasable, vd, atype, buildtype fargs) in buildtype fargs with Not_found -> DB.type_int ) @@ -1148,10 +1148,10 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = | L.Var (v) -> E.Var (v) | L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s) - | L.Lambda (P.Aerasable, _, _, body) + | L.Lambda (_, P.Aerasable, _, _, body) -> erase_type lctx (L.push_susp body (S.substitute erasure_dummy) ) - | L.Lambda (_, vdef, ty, body) + | L.Lambda (_, _, vdef, ty, body) -> let lctx' = DB.lctx_extend lctx vdef Variable ty in E.Lambda (vdef, erase_type lctx' body) @@ -1159,7 +1159,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = -> let lctx', edecls = clean_decls lctx decls in E.Let (l, edecls, erase_type lctx' body) - | L.Call (fct, args) + | L.Call (_, fct, args) -> E.Call (erase_type lctx fct, List.filter_map (clean_arg lctx) args) | L.Case (location, target, _, branches, default) @@ -1268,7 +1268,7 @@ let ctx2tup ctx nctx = let types = List.rev types in (*Log.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n");*) - mkCall (mkCons (mkInductive (loc, type_label, [], + mkCall (loc, mkCons (mkInductive (loc, type_label, [], SMap.add cons_name (List.map (fun (oname, t) -> (P.Aimplicit, oname, ===================================== src/positivity.ml ===================================== @@ -69,7 +69,7 @@ let rec positive (index : db_index) (lexp : lexp) : bool = and positive' index lexp = match Lexp.lexp_lexp' lexp with - | Lexp.Arrow (_, _, tau, _, e) + | Lexp.Arrow (_, _, _, tau, e) (* * x ⊢ e pos x ∉ fv(τ) * ────────────────────── @@ -77,7 +77,7 @@ and positive' index lexp = *) -> absent index tau && positive' (index + 1) e - | Lexp.Call (f, args) + | Lexp.Call (_, f, args) (* * x ∉ fv(e⃗) * ────────────── @@ -106,7 +106,7 @@ and positive' index lexp = && let index = index + List.length vs in Util.SMap.for_all (fun _ c -> positive_in_constructor index c) cs - | Lexp.Lambda (_, _, _, e) -> positive index e + | Lexp.Lambda (_, _, _, _, e) -> positive index e | Lexp.Susp (e, s) -> positive index (Lexp.push_susp e s ) ===================================== src/unification.ml ===================================== @@ -73,9 +73,9 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with (* ; oi (push_susp e s) *) | Let (_, defs, e) -> List.fold_left (fun o (_, e, t) -> o || oi e || oi t) (oi e) defs - | Arrow (_, _, t1, _, t2) -> oi t1 || oi t2 - | Lambda (_, _, t, e) -> oi t || oi e - | Call (f, args) + | Arrow (_, _, _, t1, t2) -> oi t1 || oi t2 + | Lambda (_, _, _, t, e) -> oi t || oi e + | Call (_, f, args) -> List.fold_left (fun o (_, arg) -> o || oi arg) (oi f) args | Inductive (_, _, args, cases) -> SMap.fold @@ -260,8 +260,8 @@ and unify' (e1: lexp) (e2: lexp) and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs : return_type = match (lexp_lexp' arrow, lexp_lexp' lxp) with - | (Arrow (var_kind1, v1, ltype1, _, lexp1), - Arrow (var_kind2, _, ltype2, _, lexp2)) + | (Arrow (_, var_kind1, v1, ltype1, lexp1), + Arrow (_, var_kind2, _, ltype2, lexp2)) -> if var_kind1 = var_kind2 then (unify' ltype1 ltype2 ctx vs) @(unify' lexp1 (srename v1 lexp2) @@ -277,8 +277,8 @@ and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs *) and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = match (lexp_lexp' lambda, lexp_lexp' lxp) with - | (Lambda (var_kind1, v1, ltype1, lexp1), - Lambda (var_kind2, _, ltype2, lexp2)) + | (Lambda (_, var_kind1, v1, ltype1, lexp1), + Lambda (_, var_kind2, _, ltype2, lexp2)) -> if var_kind1 = var_kind2 then (unify' ltype1 ltype2 ctx vs) @(unify' lexp1 lexp2 @@ -419,7 +419,7 @@ and unify_var (var: lexp) (lxp: lexp) ctx and unify_call (call: lexp) (lxp: lexp) ctx vs : return_type = match (lexp_lexp' call, lexp_lexp' lxp) with - | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2)) + | (Call (_, lxp_left, lxp_list1), Call (_, lxp_right, lxp_list2)) when OL.conv_p ctx lxp_left lxp_right -> (try List.fold_left (fun op ((ak1, e1), (ak2, e2)) -> if ak1 == ak2 then ===================================== tests/unify_test.ml ===================================== @@ -92,19 +92,19 @@ let _ = {| type Nat | Z | S (Nat); |} ectx in - let dloc = dummy_sinfo in - let nat = mkVar ((dloc, Some "Nat"), 2) in + let dsinfo = dummy_sinfo in + let nat = mkVar ((dsinfo, Some "Nat"), 2) in let shift l i = mkSusp l (S.shift i) in let ectx, _ = List.fold_left (fun (ectx, i) (name, lexp) -> - Elab.ctx_extend ectx (dloc, Some name) Variable (shift lexp i), i + 1) + Elab.ctx_extend ectx (dsinfo, Some name) Variable (shift lexp i), i + 1) (ectx, 0) - [("f", (mkArrow (Anormal, (dloc, None), nat, dloc, shift nat 1))); - ("g", (mkArrow (Anormal, (dloc, None), nat, dloc, shift nat 1))); - ("h", (mkArrow (Anormal, (dloc, Some "x"), nat, dloc, - mkArrow (Anormal, (dloc, Some "y"), shift nat 1, - dloc, shift nat 2)))); + [("f", (mkArrow (dsinfo, Anormal, (dsinfo, None), nat, shift nat 1))); + ("g", (mkArrow (dsinfo, Anormal, (dsinfo, None), nat, shift nat 1))); + ("h", (mkArrow (dsinfo, Anormal, (dsinfo, Some "x"), nat, + mkArrow (dsinfo, Anormal, (dsinfo, Some "y"), shift nat 1, + shift nat 2)))); ("a", nat); ("b", nat)] in View it on GitLab: https://gitlab.com/monnier/typer/-/commit/62b305cd4de2a96b142d96eaa92ed2d15… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/62b305cd4de2a96b142d96eaa92ed2d15… You're receiving this email because of your account on gitlab.com.

2 1

[Git][monnier/typer][master] Improve support for typelevels in inductive types
by Stefan (＠monnier) 15 Avr '22

15 Avr '22

Stefan pushed to branch master at Stefan / Typer Commits: 60431a62 by Stefan Monnier at 2022-04-15T19:30:26-04:00 Improve support for typelevels in inductive types * src/opslexp.ml (check''): Allow (erasable) typelevel fields. (get_type): Adjust accordingly. * src/log.ml (handle_error): Don't catch internal errors. * src/lexp.ml (mkSLsucc): Add some info in the error. - - - - - 3 changed files: - src/lexp.ml - src/log.ml - src/opslexp.ml Changes: ===================================== src/lexp.ml ===================================== @@ -371,7 +371,8 @@ let mkSLsucc e = match lexp_lexp' e with | SortLevel _ | Var _ | Metavar _ | Susp _ -> SLsucc e - | _ -> Log.log_fatal ~section:"internal" "SLsucc of non-level " + | _ -> Log.log_fatal ~section:"internal" "SLsucc of non-level: %s" + (lexp_head e) (********************** Lexp tests ************************) ===================================== src/log.ml ===================================== @@ -217,9 +217,11 @@ let handle_error ~(on_error : unit -> 'a) (action : unit -> 'a) : 'a = | User_error message -> show_error ("fatal user error: " ^ message); on_error () - | Internal_error message - -> show_error ("internal error: " ^ message); - on_error () + (* Don't catch these internal errors, so `OCAMLRUNPARAM=b` can + * give us a usable backtrace. + * | Internal_error message + * -> show_error ("internal error: " ^ message); + * on_error () *) let log_fatal ?section ?print_action ?loc fmt = typer_log_config.print_at_log <- true; ===================================== src/opslexp.ml ===================================== @@ -710,19 +710,25 @@ and check'' erased ctx e = (fun _ case level -> let (level, _, _, _) = List.fold_left - (fun (level, ictx, erased, n) (ak, v, t) -> - ((let lwhnf = lexp_whnf (check_type erased ictx t) ictx in - match lexp_lexp' lwhnf with + (fun (level, ictx, erased, subst) (ak, v, t) -> + let lwhnf = lexp_whnf + (check_type erased ictx t) ictx in + ((match lexp_lexp' lwhnf with | Sort (_, Stype _) when ak == P.Aerasable && impredicative_erase -> level | Sort (_, Stype level') -> mkSLlub ctx level - (* We need to unshift because the final type - * cannot refer to the fields! *) - (* FIXME: If it does refer, - * we get an ugly error! *) - (mkSusp level' (L.sunshift n)) + (mkSusp level' subst) + | Sort (_, StypeLevel) + -> (if not(ak == P.Aerasable + && impredicative_universe_poly) + then log_tc_error + ~loc:(lexp_location t) + ~print_action:(fun _ -> ()) + "Field of type %s not-allowed!" + (lexp_string t)); + level | _tt -> log_tc_error ~loc:(lexp_location t) @@ -733,8 +739,15 @@ and check'' erased ctx e = level), DB.lctx_extend ictx v Variable t, DB.set_sink 1 erased, - n + 1)) - (level, ctx, erased, 0) + (* The final type(level) cannot refer + * to the fields! *) + S.cons + (match lexp_lexp' lwhnf with + (* The non-erasable case is tested above! *) + | Sort (_, StypeLevel) -> DB.level0 + | _ -> impossible) + subst)) + (level, ctx, erased, S.identity) case in level) cases (mkSortLevel SLz) in @@ -1143,20 +1156,25 @@ and get_type ctx e = (fun _ case level -> let (level, _, _) = List.fold_left - (fun (level, ictx, n) (ak, v, t) -> - ((match lexp'_whnf (get_type ictx t) ictx with + (fun (level, ictx, subst) (ak, v, t) -> + let s = lexp'_whnf (get_type ictx t) ictx in + ((match s with | Sort (_, Stype _) when ak == P.Aerasable && impredicative_erase -> level | Sort (_, Stype level') -> mkSLlub ctx level - (* We need to unshift because the final type - * cannot refer to the fields! *) - (mkSusp level' (L.sunshift n)) + (mkSusp level' subst) | _tt -> level), DB.lctx_extend ictx v Variable t, - n + 1)) - (level, ctx, 0) + (* The final type(level) cannot refer + * to the fields! *) + S.cons + (match s with + | Sort (_, StypeLevel) -> DB.level0 + | _ -> impossible) + subst)) + (level, ctx, S.identity) case in level) cases (mkSortLevel SLz) in View it on GitLab: https://gitlab.com/monnier/typer/-/commit/60431a62a804edb74e98d08978deafc86… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/60431a62a804edb74e98d08978deafc86… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][track-sexp-lexp] redac
by Ismaila FALL (＠Fallismaila) 14 Avr '22

14 Avr '22

Ismaila FALL pushed to branch track-sexp-lexp at Stefan / Typer Commits: 3c702b98 by “falismai(a)iro.umontreal.xn--ca-02t at 2022-04-14T22:13:57+00:00 redac - - - - - 6 changed files: - + Rapport/template.tex - − redaction/Rapport Mémoire Typer.zip - src/debruijn.ml - src/debug.ml - src/lexp.ml - src/opslexp.ml Changes: ===================================== Rapport/template.tex ===================================== @@ -0,0 +1,420 @@ +\documentclass[a4paper, 12pt]{report} +\usepackage[utf8]{inputenc} +\usepackage{microtype} +\usepackage{hyperref} +\hypersetup{ + colorlinks, + citecolor = black, + filecolor = black, + linkcolor = black, + urlcolor = black +} +\usepackage{glossaries} +\makeglossaries +\usepackage{enumitem} +\usepackage{rotating} +\usepackage[colorinlistoftodos]{todonotes} +\usepackage[most]{tcolorbox} +\usepackage{afterpage} +\usepackage{amsmath} +\usepackage{graphicx} +\usepackage{url} +\usepackage[Lenny]{fncychap} +\usepackage{ulem} +\usepackage{listings} +\usepackage{upquote} +\usepackage{pxfonts} +\usepackage{tcolorbox} +\usepackage{minted} + +\tcbuselibrary{skins} +\newtcblisting{cppcode}[1][]{ + listing engine = minted, + listing only, + minted language = cpp, + minted options = {linenos=true, numbersep=3mm, texcl=true, #1}, + left = 5mm, + enhanced, + overlay = { + \begin{tcbclipinterior}\fill[black!25] (frame.south west) + rectangle ([xshift=5mm]frame.north west); + \end{tcbclipinterior}} +} +\newcommand \FOO {$`#1`$} + + + + \renewcommand{\baselinestretch}{1.5} + \usepackage{mathptmx} + \usepackage{fancyhdr} + \pagestyle{fancy} + \fancyhf{} + \chead{} + \rfoot{\thepage} + \lfoot{\tiny{Amélioration des messages d'erreurs Typer par Algorithme Génétique \\ Ismaïla Fall}} + \rhead{\fancyplain{}{\textit{\leftmark}}} + \usepackage{tabularx} + \usepackage{caption} + \usepackage[frenchb]{babel} + \usepackage{subcaption} +\addto{\captionsfrench}{ + \renewcommand{\mtctitle}{Sommaire} + \renewcommand{\tablename}{Tableau} + \renewcommand{\bibname}{Références} +} + + +\newcommand{\tabitem}{~~\llap{\textbullet}~~} + \usepackage{graphicx} + \usepackage{minitoc} + \usepackage{float} + \setcounter{secnumdepth}{3} + \setcounter{tocdepth}{2} + + + \title{Amélioration des messages d'erreurs Typer par Algorithme Génétique} +\author{Ismaïla FalIsmaïla Fal} +\date{} +\definecolor{myblue}{RGB}{51,51,153} +\newcommand\blankpage{% + \null + \thispagestyle{empty}% + \addtocounter{page}{-1}% + \newpage} + + +\newsavebox{\mybox} +\newlength{\mydepth} +\newlength{\myheight} + +\newenvironment{sidebar}% +{\begin{lrbox}{\mybox}\begin{minipage}{\textwidth}}% +{\end{minipage}\end{lrbox}% + \settodepth{\mydepth}{\usebox{\mybox}}% + \settoheight{\myheight}{\usebox{\mybox}}% + \addtolength{\myheight}{\mydepth}% + \noindent\makebox[0pt]{\hspace{-40pt}\rule[-\mydepth]{1pt}{\myheight}}% + \usebox{\mybox}} + + \newcommand{\HRule}{\rule{\linewidth}{0.4mm}} % Defines a new command for the horizontal lines, change thickness here + + +\begin{document} + +\begin{titlepage} + +\centering % Center everything on the page + +%---------------------------------------------------------------------------------------- +% HEADING SECTIONS +%---------------------------------------------------------------------------------------- + +%\textsc{\normalsize \textbf{Université de Montréal}}\\[0.3cm] % Name of your university/college +%\includegraphics[scale=.1]{img/flag}\\[0.15cm] +\text{\Large \text{Université de Montréal}}\\[1.5cm] +%\includegraphics[scale=.2]{img/ucad}\\[0.15cm] % Include a department/university logo - this will require the graphicx package +\text{\Large \text{Amélioration des messages d'erreurs Typer }}\\ % Major heading such as course name +\text{\Large \text{par Algorithme Génétique}}\\[1.5cm] % Major heading such as course name +\text{\normalsize \text{par}}\\[0.5cm] +\text{\Large {\text {Ismaïla Fall}}}\\[1cm] % Minor heading such as course title +\text{\small {\text {Département de mathématiques et de statistique }}}\\ % Minor heading such as course title +\text{\small {\text {Faculté des arts et des sciences}}}\\[2.5cm] % Minor heading such as course title + +\text{\small {\text {Mémoire présenté en vue de l’obtention du grade de }}}\\ +\text{\small {\text {Maître ès sciences (M.Sc.)}}}\\ +\text{\small {\text {en Discipline }}}\\[2.5cm] + +\text{\today}\\[2cm] + +\text{\small {\text {©Ismaila Fall, 2022}}} + +%---------------------------------------------------------------------------------------- +% DATE SECTION +%---------------------------------------------------------------------------------------- + +\end{titlepage} +\thispagestyle{empty} +\clearpage\null + +% Deuxieme page de garde + +\begin{titlepage} + +\centering % Center everything on the page + +%---------------------------------------------------------------------------------------- +% HEADING SECTIONS +%---------------------------------------------------------------------------------------- + +\text{\Large \text{Université de Montréal}}\\ +\text{\small { \uline{Faculté des arts et des sciences}}}\\[0.8cm] % Minor heading such as course title + +\text{\small {\text {Ce mémoire intitulé}}}\\[0.8cm] % Minor heading such as course title + +\text{\Large \text{Amélioration des messages d'erreurs Typer }}\\ % Major heading such as course name +\text{\Large \text{par Algorithme Génétique}}\\[1.5cm] % Major heading such as course name + +\text{\normalsize \text{présenté par}}\\[0.4cm] +\text{\Large {\text {Ismaïla Fall}}}\\[1cm] % Minor heading such as course title + + \text{\small {\text {a été évalué par un jury composé des personnes suivantes :}}}\\[1cm] % Minor heading such as course title + +\text{\small {\uline {Nom du président du jury}}}\\ +\text{\small {\text {(président-rapporteur)}}}\\ [1cm] + +\text{\small {\uline {Stefan Monnier}}}\\ +\text{\small {\text {(directeur de recherche)}}}\\ [1cm] + +\text{\small {\uline {Nom du membre de jury}}}\\ +\text{\small {\text {(membre du jury)}}}\\ [1cm] + +%---------------------------------------------------------------------------------------- +% HEADING SECTIONS +%---------------------------------------------------------------------------------------- + + +\end{titlepage} +\newpage + +\pagenumbering{roman} +\dominitoc +\chapter*{Dédicaces \markboth{Dédicaces}{}} +\markboth{DÉDICACES}{} + + +\chapter*{Remerciements \markboth{Remerciements}{}} +\markboth{REMERCIEMENTS}{} + + +\chapter*{Avant-propos \markboth{Avant-propos}{}} + + +\tableofcontents +\chapter*{Sigles et Abréviations \markboth{Sigles et Abréviations}{}} + +\listoffigures +\listoftables + +%---------------------------------------------------------------------------------------- +% Resume +%---------------------------------------------------------------------------------------- + +\chapter*{Résumé \markboth{Résumé}{}} +Le défi majeur des programmeurs (plus précisément des novices) sont les messages d'erreur du compilateur. Nous nous intéressons au problème d'affichage de bon message d'erreur de compilation. Dans certains langages comme Typer, la vérification du type des expressions est faite lors de la compilation; ce qui oblige le compilateur à déduire les types de certaines ou de toutes les expressions; mais aussi d'envisager la meilleure manière d'écrire le type (dans le langage source) dans un message d'erreur. Cependant l'interprétation du type des expressions faite par le compilateur est toujours diffèrent de ce que l'utilisateur aimerait voir en cas d'erreur de compilation. En effet, il n'existe pas d'algorithme déterministe permettant de trouver une représentation naturelle dans le code source correspondant à la représentation interne d'un type. D'où l'importance d'implémenter un système heuristique tel que les algorithmes génétiques où les réseaux de neurones qui nous donne cette information; permettant ainsi un meilleur affichage du texte des messages d'erreur. Donc, nous avons décidé de travailler sur l'amélioration des messages d'erreur du compilateur Typer, dans sa phase de traduction du langage (interprétation et représentation des différents expressions dans le langage source) en proposant une approche `algorithme génétique`.\\ +\textbf{Mots Clés: Message d'erreur, Typer, Algorithme génétique, Compilateur} + + +%---------------------------------------------------------------------------------------- +% Abstract +%---------------------------------------------------------------------------------------- + +\chapter*{Abstract \markboth{Abstract}{}} +The major challenge for programmers (more precisely for novices) are compiler error messages. We are interested in the problem of displaying a good compiler error message. In some languages like Typer, the type checking of expressions is done at compile time; this forces the compiler to deduce the types of some or all expressions; but also to consider the best way to write the type (in the source language) in an error message. However, the compiler's interpretation of the type of expressions is always different from what the user would like to see in case of a compiler error. Indeed, there is no deterministic algorithm allowing to find a natural representation in the source code corresponding to the internal representation of a type. Hence the importance of implementing a heuristic system such as genetic algorithms or neural networks that gives us this information; thus allowing a better display of the text of error messages. So, we decided to work on the improvement of the error messages of the Typer compiler, in its language translation phase (interpretation and representation of the different expressions in the source language) by proposing a `genetic algorithm` approach.\\ +\textbf{Keywords: Error message, Typer, Genetic algorithm, Compiler} + +%\chapter*{Introduction \markboth{Introduction}{}} \mtcaddchapter +\newpage +\null +\newpage +%\addcontentsline{toc}{chapter}{Introduction} + +%---------------------------------------------------------------------------------------- +% Chapitre 1 +%---------------------------------------------------------------------------------------- +\pagenumbering{arabic} +% CHAPITRE 1 +\chapter{Introduction Générale} +\textit{\textbf{Résumé:} \\ +Dans ce chapitre, nous faisons une description de notre sujet en dégageant le contexte, la problématique ainsi que les objectifs que nous nous sommes fixes. Enfin, de bien mettre en avant le travail réalisé, nous présenterons les différents chapitres de ce mémoires. +} +\setcounter{minitocdepth}{2} +\minitoc +\newpage + +\section{Contexte} +Typer est un langage de programmation fortement typé qui appartient à la famille ML. La vérification de type statique faite lors de la compilation lui permet de fournir une sécurité de type au programmeur. Comme beaucoup de langage fonctionnelle, le système de type de Typer est inspiré en grand parti du système de type Hindley-Milner. \\ +Le système de type Hindley-Milner combiné avec les macros expansions forment la partie élaboration (compilateur) de Typer. Cette combinaison de polymorphisme et d'interface de type permet de définir de nouveau type de donnée, augmentant ainsi la productivité des programmeurs mais aussi la fiabilité du système de type. Cependant elle n'est pas sans inconvénient, le signalement des messages d'erreur de type devient plus difficile. En effet, le compilateur n'indique pas précisément la source de l'erreur de type; mais aussi il arrive généralement que les types inférés ne correspondent pas aux types voulus. C'est dans cette optique qu'on nous a confié la tâche de proposer une solution algorithme génétique pour tenter d'amélioration les messages d'erreur du compilateur Typer. + + +\section{Problématique} +Implémenter à base par un langage similaire à Coq, Typer utilise un système de type dépendant, qu'il combine avec un système de macro puissant. Ce qui permet d'étendre le langage via la méta-programmation de manière transparente.\\ +Cependant ce système de typage dépendant combiné avec la méta-programmation faite qu'on a un sérieux problème d'afficher de bon message d'erreur (généralement des erreurs de type). Mais d'autres problèmes supplémentaires viennent de certaines détails de Typer (tel que l'absence de mot réservés) qui implique que le type d'une valeur peut dépendre d'une autre valeur obtenue qu'au moment de la compilation. \\ +Prenons par exemple la définition de type suivante: +\begin{cppcode} +type List (a : Type) + | nil + | cons (hd : a)(tl : List a); +\end{cppcode} + +Dans ce extrait, nous avons une fonction \FOO{List} qui prend en argument $`a`$ qui est un type et renvoie un nouveau type \FOO{List a}. Ce nouveau type est décrit comme étant formé soit de la constante $`nil`$ c'est-à-dire la liste vide; soit d'une valeur de la forme \mathit{`cons hd tl`} ou \mathit{`cons`} est un tag qui permet de reconnaître cette valeur, $`hd`$ est le premier élément de la liste et $`tl`$ est une référence qui pointe vers le reste de la liste.\\ +Examinons la déclaration suivante: +\begin{cppcode} + x = cons 1 nil; +\end{cppcode} + +Nous avons dans $`x`$ une liste qui contient juste un entier (le chiffre 1). $`x`$ est de type \FOO{List Int}, qui est la représentation que le programmeur aimerait voir, dans Typer, mais au contraire il aura à la place un type qui représente plutôt à quelques choses comme ça : +\begin{cppcode} + typecons <qqch> (nil)(cons (hd : ##Int)(tl : List ##Int)) +\end{cppcode} + +Cette ligne incompréhensible pour le programmeur est le résultat de l'élaboration du code source, qui équivaut à \FOO{List Int} et donc ce sont deux représentations différentes du même type. Très souvent, ce résultat est diffèrent du code source. Au pire la bonne représentation qu'on aimerait utiliser (comme dans notre exemple \FOO{List Int}) n'est souvent présent nulle part dans le code source.\\ +Dès lors, le problème qui se pose est comment transformer la forme incompréhensible en quelques choses comme \FOO{List Int}. + + +\section{Contributions} +Dans le but de proposer une solution au problème cité ci-dessus, notre contributions est de réaliser un système heuristique basé sur les algorithmes génétiques qui permettent au compilateur Typer de faire une meilleur représentation des messages d'erreur. Pour y arriver, nous nous sommes fixe des objectifs spécifiques, listés ci-dessous: +\begin{itemize} + \item[\Rightarrow] Apporter quelques modifications au compilateur en extrayant des informations utiles sur certaines parties. + + \item[\Rightarrow] Collecter et organiser quelques données qui nous permettrons d'entraîner et de tester notre système heuristique. + + \item[\Rightarrow] Implémenter un algorithme génétique pour mettre au compilateur Typer de générer de meilleur message d'erreur, compréhensible pour le programmeur. +\end{itemize} +\vspace{10pt} + + +\section{Plan} +Dans le but de bien mettre en avant le travail réalisé, nous structurons ce mémoire en quart (04) chapitres: +\begin{enumerate} + \item \textbf{État de l'art} : Il s'agit dans ce chapitre de faire une présentation des caractéristiques de notre projet. Dans un premier temps, nous faisons une synthèse des travaux étroitement liées à notre projet d'étude; ensuite, nous présenterons Typer plus précisément de son compilation. En troisième point, nous les systèmes heuristiques seront visités particulièrement les algorithmes génétiques. + + \item \textbf{Implémentions de la solution} : pour ce chapitre, il sera question d'exposer la stratégie de collection des données et la mise en oeuvre de la solution. + + \item \textbf{Évaluation du résultat } : ce chapitre permet de dévaluer l'aspect de notre travail. + + \item \textbf{Conclusion} : Finalement, ce chapitre permet d'exposer nos conclusions avant de finir par les limites et perspectives. \\ \\ +\end{enumerate} + +\textit{\textbf{Synthèse:} \\ + Dans ce chapitre, nous avons décrit notre sujet de recherche en dégageant le contexte, la problématique et les objectifs. Nous y avons aussi profité pour présenter les différents chapitres qui composent notre mémoire. \\ +Cependant, il a toujours été difficile de déduire la source d'un erreur à partir du message générer par le compilateur. Le prochaine chapitre fera donc l'objet d'une synthèse détail des études existant en rapport avec nos travaux; suivi de la présentation de Typer et des algorithmes génétiques. +} + + +%---------------------------------------------------------------------------------------- +% Chapitre 2 +%---------------------------------------------------------------------------------------- + +%CHAPITRE 2 +\chapter{ État de l'art } +\textit{\textbf{Résumé:} Ce chapitre consiste à mettre l'accent sur l'état de l'art des erreurs de compilations. Il s'agit de faire une synthèse de quelques travaux connexes qui essayent d'améliorer les messages d'erreur génère par le compilateur; de présenter ensuite le langage Typer ainsi que son compilateur et enfin nous finissons par parler des systèmes heuristiques particulièrement des algorithmes génétiques. +} +\setcounter{minitocdepth}{1} +\minitoc +\newpage + +\section{Travaux Connexes} +Un langage de programmation avec un système de type permet d'assurer le programmeur sur l'exactitude de son programme; elle permet au compilateur de rejeter les programmes non typé ou mal typés. Mais le problème de beaucoup de programmeur survient lorsque le compilateur rejette leur programme; en effet le processus de débogage est souvent fastidieux et inefficace. C'est dans cette optique que beaucoup de travaux ont vu le jour + + + +\section{Présentation de Typer} +\subsection{Structure de Typer} + +\subsection{Élaboration} +\subsubsection{Macro-expansions} +\subsubsection{Inférence de Type} + + + +\section{Les Algorithmes génétiques} +\subsection{les systèmes heuristiques} +\subsection{les algorithmes génétiques} + + +\textit{\textbf{Synthèse:} \\ +conclusion +} + + +%---------------------------------------------------------------------------------------- +% Chapitre 3 +%---------------------------------------------------------------------------------------- + +%CHAPITRE 3 +%\chapter{ Aperçu de Typer } +%\textit{\textbf{Résumé:} } +%\setcounter{minitocdepth}{1} +%\minitoc + +%\section{Définitions des concepts du domaine} + +%\section{Fonctionnalités existantes} +%\subsection{Les modules existants} + +%\section{Architecture et Technologies utilisées} +%\subsection{Architecture technique} +%\subsection{Architecture applicative} + + + +%---------------------------------------------------------------------------------------- +% Chapitre 4 +%---------------------------------------------------------------------------------------- + +%CHAPITRE 4 +%\chapter{Les algorithmes génétiques} +%\textit{\textbf{Résumé:}} +%\setcounter{minitocdepth}{2} +%\minitoc +%\section{Les acteurs de l'application} +%\section{Présentation du domaine} + +%---------------------------------------------------------------------------------------- +% Chapitre 5 +%---------------------------------------------------------------------------------------- + +%CHAPITRE 5 +\chapter{Implémentions de la solution} +\textit{\textbf{Résumé : }} +\setcounter{minitocdepth}{1} +\minitoc +\newpage +\section{Solution technique} + +\section{Architecture de la plateforme} + + +%---------------------------------------------------------------------------------------- +% Chapitre 6 +%---------------------------------------------------------------------------------------- + + +%CHAPITRE 6 +\chapter{Évaluation du résultat} +\textit{\textbf{Résumé:} } +\minitoc +\newpage + + + +%---------------------------------------------------------------------------------------- +% Chapitre 7 +%---------------------------------------------------------------------------------------- + +%CHAPITRE 7 +\chapter{Conclusion et Perspectives} +\textit{\textbf{Résumé:} } +\minitoc +\newpage + +%\chapter*{Conclusion et Perspectives} \mtcaddchapter +%\markboth{Conclusion et Perspectives}{} +%\addcontentsline{toc}{ch1apter}{Conclusion et Perspectives} + +\bibliographystyle{plain} +\bibliography{biblio} + +\chapter*{Annexes} \mtcaddchapter +\addcontentsline{toc}{chapter}{Annexes} +\markboth{Annexes}{} +\newpage + + +\section*{Résumé \markboth{}{}} +\thispagestyle{empty} + + +\section*{Abstract \markboth{}{}} + +\end{document} ===================================== redaction/Rapport Mémoire Typer.zip deleted ===================================== Binary files "a/redaction/Rapport M\303\251moire Typer.zip" and /dev/null differ ===================================== src/debruijn.ml ===================================== @@ -368,17 +368,16 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = else fun () -> summarize_lctx ctx dbi in fatal - ~loc ~print_action + ~loc:(sexp_location loc) ~print_action ({|DeBruijn index %d refers to wrong name. |} ^^ {|Expected: "%s" got "%s"|}) dbi ename name | _ -> () in - ret with | Not_found -> fatal - ~loc "DeBruijn index %d of `%s` out of bounds" dbi (maybename oename) + ~loc:(sexp_location loc) "DeBruijn index %d of `%s` out of bounds" dbi (maybename oename) let lctx_lookup_type (ctx : lexp_context) (vref : vref) : lexp = let (_, i) = vref in ===================================== src/debug.ml ===================================== @@ -137,7 +137,7 @@ let debug_lexp_decls decls = let str = match str with | scd :: tl - -> printf " FILE: %-25s : %s\n" loc.file scd; + -> printf " FILE: %-25s : %s\n" (Source.Location.to_string (sexp_location loc)) scd; tl | _ -> [] in ===================================== src/lexp.ml ===================================== @@ -540,7 +540,7 @@ let rec lexp_location e = (********* Normalizing a term *********) -let vdummy = (U.dummy_location, None) +let vdummy = (dummy_sinfo, None) let maybename n = match n with None -> "<anon>" | Some v -> v let sname (l, n) = (sexp_location l, maybename n) ===================================== src/opslexp.ml ===================================== @@ -230,7 +230,7 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = -> let subst = S.cons (get_refl e') (S.substitute e') in lexp_whnf_aux (push_susp default subst ) ctx | _ -> Log.log_error - ~section:"WHNF" ~loc:l + ~section:"WHNF" ~loc:(sexp_location l) {|Unhandled constructor "%s" in case expression|} name; mkCase (l, e, rt, branches, default) in (match lexp_lexp' e' with @@ -413,7 +413,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let ekind = get_type ctx etype in let elvl = match lexp'_whnf ekind ctx with | Sort (_, Stype l) -> l - | _ -> Log.log_fatal ~loc:(lexp_location ekind) + | _ -> Log.log_fatal ~loc:(sexp_location (lexp_location ekind)) "Target lexp's kind is not a sort"; in (* 1. Get the inductive for the field types *) let it, aargs = match lexp_lexp' etype with @@ -468,7 +468,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let subst = S.shift offset in let eaargs = List.map (fun (_, a) -> (P.Aerasable, a)) aargs in - let ctor = mkSusp (mkCall (mkCons (it, (DB.dloc, l1)) , + let ctor = mkSusp (mkCall (mkCons (it, (sexp_location (DB.dloc), l1)) , eaargs) ) subst in let hlxp = mkCall (ctor, args) in let nctx = ctx_extend_with_eq nctx subst hlxp in @@ -589,7 +589,7 @@ and check'' erased ctx e = if conv_p ctx t t' then () else log_tc_error - ~loc:(lexp_location e) + ~loc:(sexp_location (lexp_location e)) "Type mismatch for %s : %s != %s" (lexp_string e) (lexp_string t) (lexp_string t') in @@ -599,14 +599,14 @@ and check'' erased ctx e = | Sort _ -> () | _ -> let loc = lexp_location t in - log_tc_error ~loc "Not a proper type: %s" (lexp_string t)); + log_tc_error ~loc:(sexp_location loc) "Not a proper type: %s" (lexp_string t)); s in match lexp_lexp' e with | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _) | Symbol _ | Node (_, _)) - -> (log_tc_error ~loc:(lexp_location e) "Unsupported immediate value!"; + -> (log_tc_error ~loc:(sexp_location (lexp_location e)) "Unsupported immediate value!"; DB.type_int ) | SortLevel SLz -> DB.type_level | SortLevel (SLsucc e) @@ -637,7 +637,7 @@ and check'' erased ctx e = | Var (((loc, name), idx) as v) -> if DB.set_mem idx erased then log_tc_error - ~loc + ~loc:(sexp_location loc) {|Var `%s` can't be used here, because it's erasable|} (maybename name) ; lookup_type ctx v @@ -670,13 +670,13 @@ and check'' erased ctx e = match sort_compose ctx nctx loc ak k1 k2 with | SortResult k -> k | SortInvalid - -> log_tc_error ~loc "Invalid arrow: inner TypelLevel argument"; + -> log_tc_error ~loc:(sexp_location loc) "Invalid arrow: inner TypelLevel argument"; mkSort (loc, StypeOmega) | SortK1NotType - -> log_tc_error ~loc:(lexp_location t1) "Not a proper type"; + -> log_tc_error ~loc:(sexp_location (lexp_location t1)) "Not a proper type"; mkSort (loc, StypeOmega) | SortK2NotType - -> log_tc_error ~loc:(lexp_location t2) "Not a proper type"; + -> log_tc_error ~loc:(sexp_location (lexp_location t2)) "Not a proper type"; mkSort (loc, StypeOmega) ) | Lambda (ak, ((l,_) as v), t, e) -> (let _k = check_type DB.set_empty ctx t in @@ -693,11 +693,11 @@ and check'' erased ctx e = match lexp'_whnf ft ctx with | Arrow (ak', _v, t1, _l, t2) -> if ak != ak' - then log_tc_error ~loc:(lexp_location arg) "arg kind mismatch"; + then log_tc_error ~loc:(sexp_location (lexp_location arg)) "arg kind mismatch"; assert_type ctx arg at t1; mkSusp t2 (S.substitute arg) | _ -> log_tc_error - ~loc:(lexp_location arg) + ~loc:(sexp_location (lexp_location arg)) "Calling a non functin (type = %s)!" (lexp_string ft); ft) ft args @@ -725,7 +725,7 @@ and check'' erased ctx e = (mkSusp level' (L.sunshift n) ) | _tt -> log_tc_error - ~loc:(lexp_location t) + ~loc:(sexp_location (lexp_location t)) ~print_action:(fun _ -> DB.print_lexp_ctx ictx; print_newline ()) "Field type %s is not a Type! (%s)" @@ -759,7 +759,7 @@ and check'' erased ctx e = let ekind = get_type ctx etype in let elvl = match lexp'_whnf ekind ctx with | Sort (_, Stype l) -> l - | _ -> Log.log_error ~loc:(lexp_location ekind) + | _ -> Log.log_error ~loc:(sexp_location (lexp_location ekind)) "Target lexp's kind is not a sort"; DB.level0 in let it, aargs = call_split etype in (match lexp'_whnf it ctx, aargs with @@ -772,7 +772,7 @@ and check'' erased ctx e = * returns a valid type. *) -> mksubst (S.cons aarg s) fargs aargs | _ - -> log_tc_error ~loc:l "Wrong arg number to inductive type!"; + -> log_tc_error ~loc:(sexp_location l) "Wrong arg number to inductive type!"; s in let s = mksubst S.identity fargs aargs in let ctx_extend_with_eq ctx subst hlxp nerased = View it on GitLab: https://gitlab.com/monnier/typer/-/commit/3c702b98d43ea8e528c36a54884fc9aa1… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/3c702b98d43ea8e528c36a54884fc9aa1… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][track-sexp-lexp] redac
by Ismaila FALL (＠Fallismaila) 13 Avr '22

13 Avr '22

Ismaila FALL pushed to branch track-sexp-lexp at Stefan / Typer Commits: 96adbad9 by “falismai(a)iro.umontreal.xn--ca-02t at 2022-04-13T20:02:44+00:00 redac - - - - - 10 changed files: - + .idea/misc.xml - + redaction/Rapport Mémoire Typer.zip - src/debruijn.ml - src/debug.ml - src/elexp.ml - src/inverse_subst.ml - src/lexp.ml - src/pexp.ml - src/sexp.ml - src/util.ml Changes: ===================================== .idea/misc.xml ===================================== @@ -0,0 +1,8 @@ +<?xml version="1.0" encoding="UTF-8"?> +<project version="4"> + <component name="SwUserDefinedSpecifications"> + <option name="specTypeByUrl"> + <map /> + </option> + </component> +</project> \ No newline at end of file ===================================== redaction/Rapport Mémoire Typer.zip ===================================== Binary files /dev/null and "b/redaction/Rapport M\303\251moire Typer.zip" differ ===================================== src/debruijn.ml ===================================== @@ -35,10 +35,10 @@ module Str = Str open Util - - open Lexp +open Sexp + module M = Myers open Fmt @@ -83,21 +83,21 @@ let fatal ?print_action ?loc fmt = (* Type definitions * ---------------------------------- *) -let dloc = dummy_location +let dloc = dummy_sinfo let type_level_sort = mkSort (dloc, StypeLevel) let sort_omega = mkSort (dloc, StypeOmega) -let type_level = mkBuiltin ((dloc, "TypeLevel"), type_level_sort) +let type_level = mkBuiltin ((sexp_location dloc, "TypeLevel"), type_level_sort) let level0 = mkSortLevel SLz let level1 = mkSortLevel (mkSLsucc level0) let level2 = mkSortLevel (mkSLsucc level1) let type0 = mkSort (dloc, Stype level0) let type1 = mkSort (dloc, Stype level1) let type2 = mkSort (dloc, Stype level2) -let type_int = mkBuiltin ((dloc, "Int"), type0) -let type_integer = mkBuiltin ((dloc, "Integer"), type0) -let type_float = mkBuiltin ((dloc, "Float"), type0) -let type_string = mkBuiltin ((dloc, "String"), type0) -let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0) +let type_int = mkBuiltin ((sexp_location dloc, "Int"), type0) +let type_integer = mkBuiltin ((sexp_location dloc, "Integer"), type0) +let type_float = mkBuiltin ((sexp_location dloc, "Float"), type0) +let type_string = mkBuiltin ((sexp_location dloc, "String"), type0) +let type_elabctx = mkBuiltin ((sexp_location dloc, "Elab_Context"), type0) let type_eq_type = let lv = (dloc, Some "l") in let tv = (dloc, Some "t") in @@ -111,13 +111,13 @@ let type_eq_type = mkVar (tv, 1) , dloc, mkSort (dloc, Stype (mkVar (lv, 3))))))) -let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) +let type_eq = mkBuiltin ((sexp_location dloc, "Eq"), type_eq_type) let eq_refl = let lv = (dloc, Some "l") in let tv = (dloc, Some "t") in let xv = (dloc, Some "x") in - mkBuiltin ((dloc, "Eq.refl"), + mkBuiltin ((sexp_location dloc, "Eq.refl"), mkArrow (Aerasable, lv, type_level, dloc, mkArrow (Aerasable, tv, ===================================== src/debug.ml ===================================== @@ -119,9 +119,9 @@ let debug_pexp_print ptop = let debug_lexp_decls decls = let sep = " : " in List.iter (fun e -> - let ((loc, _name), lxp, _ltp) = e in + let (((loc: sinfo), _name), lxp, _ltp) = e in - printf "%-15s[%s]" (lexp_name lxp) (Source.Location.to_string loc); + printf "%-15s[%s]" (lexp_name lxp) (Source.Location.to_string (sexp_location loc)); let str = lexp_str_decls (!debug_ppctx) [e] in ===================================== src/elexp.ml ===================================== @@ -36,8 +36,8 @@ open Sexp (* Sexp type *) module U = Util module L = Lexp -type vname = U.vname -type vref = U.vref +type vname = Sexp.vname +type vref = Sexp.vref type label = symbol module SMap = U.SMap @@ -53,7 +53,7 @@ type elexp = | Var of vref (* Recursive `let` binding. *) - | Let of U.location * (vname * elexp) list * elexp + | Let of sinfo * (vname * elexp) list * elexp (* An anonymous function. *) | Lambda of vname * elexp @@ -71,8 +71,8 @@ type elexp = * Case (l, e, branches, default) * tests the value of `e`, and either selects the corresponding branch * in `branches` or branches to the `default`. *) - | Case of U.location * elexp - * (U.location * vname list * elexp) SMap.t + | Case of sinfo * elexp + * (sinfo * vname list * elexp) SMap.t * (vname * elexp) option (* A Type expression. There's no useful operation we can apply to it, @@ -82,14 +82,14 @@ type elexp = let rec elexp_location e = match e with | Imm s -> sexp_location s - | Var ((l,_), _) -> l + | Var ((l,_), _) -> sexp_location l | Builtin ((l, _)) -> l - | Let (l,_,_) -> l - | Lambda ((l,_),_) -> l + | Let (l,_,_) -> sexp_location l + | Lambda ((l,_),_) -> sexp_location l | Call (f,_) -> elexp_location f | Cons (_, (l, _)) -> l - | Case (l,_,_,_) -> l - | Type e -> L.lexp_location e + | Case (l,_,_,_) -> sexp_location l + | Type e -> sexp_location (L.lexp_location e) let elexp_name e = ===================================== src/inverse_subst.ml ===================================== @@ -42,6 +42,7 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) open Lexp open Util module S = Subst +open Sexp (** Provide inverse function for computing the inverse of a substitution *) @@ -94,7 +95,7 @@ let sizeOf (s: (int * int) list): int = List.length s let counter = ref 0 let mkVar (idx: int) : lexp = counter := !counter + 1; - mkVar ((U.dummy_location, None), idx) + mkVar ((dummy_sinfo, None), idx) (** Fill the gap between e_i in the list of couple (e_i, i) by adding dummy variables. ===================================== src/lexp.ml ===================================== @@ -33,8 +33,8 @@ open Grammar (* open Unify *) module S = Subst -type vname = U.vname -type vref = U.vref +type vname = Sexp.vname +type vref = Sexp.vref type meta_id = int (* Identifier of a meta variable. *) type sinfo = sexp @@ -172,6 +172,14 @@ let metavar_lookup (id : meta_id) : metavar_info with Not_found -> Log.log_fatal ~section:"LEXP" "metavar lookup failure!" + + + + + + + + (********************** Hash-consing **********************) (** Hash-consing test ** @@ -516,25 +524,25 @@ let rec lexp_location e = | SortLevel (SLlub (e, _)) -> lexp_location e | SortLevel SLz -> dummy_sinfo | Imm s -> s - | Var ((l,_),_) -> dummy_sinfo - | Builtin ((l, _), _) -> dummy_sinfo + | Var ((_l,_),_) -> dummy_sinfo + | Builtin ((_l, _), _) -> dummy_sinfo | Let (l,_,_) -> l | Arrow (_,_,_,l,_) -> l - | Lambda (_,(l,_),_,_) -> dummy_sinfo + | Lambda (_,(_l,_),_,_) -> dummy_sinfo | Call (f,_) -> lexp_location f | Inductive (l,_,_,_) -> l - | Cons (_,(l,_)) -> dummy_sinfo + | Cons (_,(_l,_)) -> dummy_sinfo | Case (l,_,_,_,_) -> l | Susp (e, _) -> lexp_location e (* | Susp (_, e) -> lexp_location e *) - | Metavar (_,_,(l,_)) -> dummy_sinfo + | Metavar (_,_,(_l,_)) -> dummy_sinfo (********* Normalizing a term *********) let vdummy = (U.dummy_location, None) let maybename n = match n with None -> "<anon>" | Some v -> v -let sname (l,n) = (l, maybename n) +let sname (l, n) = (sexp_location l, maybename n) let rec push_susp e s = (* Push a suspension one level down. *) match lexp_lexp' e with @@ -577,7 +585,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) | Cons (it, name) -> mkCons (mkSusp it s , name) | Case (l, e, ret, cases, default) -> mkCase (l, mkSusp e s , mkSusp ret s , - SMap.map (fun ((l: sinfo), cargs, e) + SMap.map (fun (l, cargs, e) -> let s' = L.fold_left (fun s (_,ov) -> ssink ov s) s cargs in @@ -674,27 +682,27 @@ let rec lexp_unparse lxp = | Imm (sexp) -> sexp | Builtin ((l,name), _) -> Symbol (l, "##" ^ name) (* FIXME: Add a Sexp syntax for debindex references. *) - | Var ((loc, name), _) -> Symbol (loc, maybename name) + | Var ((loc, name), _) -> Symbol (sexp_location loc, maybename name) | Cons (t, (l, name)) -> Node (sdatacons, [lexp_unparse t; Symbol (l, name)]) | Lambda (kind, vdef, ltp, body) -> let l = lexp_location lxp in let st = lexp_unparse ltp in - Node (Symbol (l, match kind with + Node (Symbol (sexp_location l, match kind with | Anormal -> "lambda_->_" | Aimplicit -> "lambda_=>_" | Aerasable -> "lambda_≡>_"), - [Node (Symbol (l, "_:_"), [Symbol (sname vdef); st]); + [Node (Symbol (sexp_location l, "_:_"), [Symbol (sname vdef); st]); lexp_unparse body ]) | Arrow (arg_kind, (l,oname), ltp1, loc, ltp2) -> let ut1 = lexp_unparse ltp1 in - Node (Symbol (loc, match arg_kind with Anormal -> "_->_" + Node (Symbol (sexp_location loc, match arg_kind with Anormal -> "_->_" | Aimplicit -> "_=>_" | Aerasable -> "_≡>_"), [(match oname with None -> ut1 - | Some v -> Node (Symbol (l, "_:_"), - [Symbol (l,v); ut1])); + | Some v -> Node (Symbol (sexp_location l, "_:_"), + [Symbol (sexp_location l,v); ut1])); lexp_unparse ltp2 ]) | Let (loc, ldecls, body) @@ -707,7 +715,7 @@ let rec lexp_unparse lxp = [Symbol (sname vdef); lexp_unparse lxp ]) :: acc) [] ldecls in - Node (Symbol (loc, "let_in_"), + Node (Symbol (sexp_location loc, "let_in_"), [Node (Symbol (U.dummy_location, "_;_"), sdecls); lexp_unparse body ]) @@ -725,7 +733,7 @@ let rec lexp_unparse lxp = Node (Symbol label, List.map pexp_u_formal_arg pfargs) :: List.map (fun (name, types) - -> Node (Symbol (loc, name), + -> Node (Symbol (sexp_location loc, name), List.map (fun arg -> match arg with @@ -749,13 +757,13 @@ let rec lexp_unparse lxp = let pat_args = List.map (fun (_kind, ((l,oname) as name)) -> match oname with - | Some vdef -> (Some (l,vdef), name) + | Some vdef -> (Some (sexp_location l, vdef), name) | None -> (None, name)) args (* FIXME: Rather than a Pcons we'd like to refer to an existing * binding with that value! *) in (Ppatcons (Node (sdatacons, - [bt; Symbol (loc, str)]), + [bt; Symbol (sexp_location loc, str)]), pat_args), lexp_unparse bch ) ) (SMap.bindings branches) in @@ -765,29 +773,29 @@ let rec lexp_unparse lxp = lexp_unparse dft )::pbranch | None -> pbranch in let e = lexp_unparse target in - Node (Symbol (loc, "case_"), + Node (Symbol (sexp_location loc, "case_"), e :: List.map (fun (pat, branch) -> - Node (Symbol (pexp_pat_location pat, "_=>_"), + Node (Symbol (sexp_location (pexp_pat_location pat), "_=>_"), [pexp_u_pat pat; branch])) pbranch) (* FIXME: The cases below are all broken! *) | Metavar (idx, subst, (loc, name)) - -> Symbol (loc, "?" ^ (maybename name) ^ "-" ^ string_of_int idx + -> Symbol (sexp_location loc, "?" ^ (maybename name) ^ "-" ^ string_of_int idx ^ "[" ^ subst_string subst ^ "]") | SortLevel (SLz) -> Symbol (U.dummy_location, "##TypeLevel.z") | SortLevel (SLsucc l) - -> Node (Symbol (lexp_location l, "##TypeLevel.succ"), + -> Node (Symbol (sexp_location (lexp_location l), "##TypeLevel.succ"), [lexp_unparse l]) | SortLevel (SLlub (l1, l2)) - -> Node (Symbol (lexp_location l1, "##TypeLevel.∪"), + -> Node (Symbol (sexp_location (lexp_location l1), "##TypeLevel.∪"), [lexp_unparse l1 ; lexp_unparse l2 ]) - | Sort (l, StypeOmega) -> Symbol (l, "##Type_ω") - | Sort (l, StypeLevel) -> Symbol (l, "##TypeLevel.Sort") + | Sort (l, StypeOmega) -> Symbol (sexp_location l, "##Type_ω") + | Sort (l, StypeLevel) -> Symbol (sexp_location l, "##TypeLevel.Sort") | Sort (_l, Stype sl) - -> Node (Symbol (lexp_location sl, "##Type_"), + -> Node (Symbol (sexp_location (lexp_location sl), "##Type_"), [lexp_unparse sl ]) (* FIXME: ¡Unify lexp_print and lexp_string! *) ===================================== src/pexp.ml ===================================== @@ -20,7 +20,7 @@ more details. You should have received a copy of the GNU General Public License along with this program. If not, see <http://www.gnu.org/licenses/>. *) -open Util +(*open Util*) open Sexp (* Symbol *) let pexp_error loc = Log.log_error ~section:"PEXP" ~loc @@ -43,7 +43,7 @@ type ppat = let pexp_pat_location e = match e with | Ppatsym (l,_) -> l - | Ppatcons (e, _) -> sexp_location e + | Ppatcons (e, _) -> e let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = match arg with @@ -56,28 +56,28 @@ let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = | None -> Symbol (l, "_")]) let pexp_p_pat_arg (s : sexp) = match s with - | Symbol (l , n) -> (None, (l, match n with "_" -> None | _ -> Some n)) - | Node (Symbol (_, "_:=_"), [Symbol f; Symbol (l,n)]) - -> (Some f, (l, Some n)) + | Symbol (_l , n) -> (None, (s, match n with "_" -> None | _ -> Some n)) + | Node (Symbol (_, "_:=_"), [Symbol f; Symbol (_l,n)]) + -> (Some f, (s, Some n)) | _ -> let loc = sexp_location s in pexp_error loc "Unknown pattern arg"; - (None, (loc, None)) + (None, (s, None)) let pexp_u_pat_arg ((okn, (l, oname)) : symbol option * vname) : sexp = - let pname = Symbol (l, match oname with None -> "_" | Some n -> n) in + let pname = Symbol (sexp_location l, match oname with None -> "_" | Some n -> n) in match okn with | None -> pname | Some ((l,_) as n) -> Node (Symbol (l, "_:=_"), [Symbol n; pname]) let pexp_p_pat (s : sexp) : ppat = match s with - | Symbol (l, n) -> Ppatsym (l, match n with "_" -> None | _ -> Some n) + | Symbol (_l, n) -> Ppatsym (s, match n with "_" -> None | _ -> Some n) | Node (c, args) -> Ppatcons (c, List.map pexp_p_pat_arg args) | _ -> let l = sexp_location s in - pexp_error l "Unknown pattern"; Ppatsym (l, None) + pexp_error l "Unknown pattern"; Ppatsym (s, None) let pexp_u_pat (p : ppat) : sexp = match p with - | Ppatsym (l, None) -> Symbol (l, "_") - | Ppatsym (l, Some n) -> Symbol (l, n) + | Ppatsym (l, None) -> Symbol (sexp_location l, "_") + | Ppatsym (l, Some n) -> Symbol (sexp_location l, n) | Ppatcons (c, args) -> Node (c, List.map pexp_u_pat_arg args) ===================================== src/sexp.ml ===================================== @@ -39,8 +39,15 @@ type sexp = (* Syntactic expression, kind of like Lisp. *) | Node of sexp * sexp list type token = sexp +type sinfo = sexp +type vname = sinfo * string option +type vref = vname * db_index (*Name redundancy*) + + + let epsilon l = Symbol (l, "") let dummy_epsilon = epsilon dummy_location + let dummy_sinfo = epsilon dummy_location (********************** Sexp tests **********************) ===================================== src/util.ml ===================================== @@ -33,11 +33,9 @@ let dummy_location = Source.Location.dummy (* Occurrence of a variable's symbol: we use DeBruijn index, and for * debugging purposes, we remember the name that was used in the source * code. *) -type vname = location * string option type db_index = int (* DeBruijn index. *) type db_offset = int (* DeBruijn index offset. *) type db_revindex = int (* DeBruijn index counting from the root. *) -type vref = vname * db_index type bottom = | B_o_t_t_o_m_ of bottom View it on GitLab: https://gitlab.com/monnier/typer/-/commit/96adbad9c495b49e977ef61778b70cae2… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/96adbad9c495b49e977ef61778b70cae2… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][track-sexp-lexp] location -> sinfo
by Ismaila FALL (＠Fallismaila) 03 Avr '22

03 Avr '22

Ismaila FALL pushed to branch track-sexp-lexp at Stefan / Typer Commits: 967baf86 by “falismai(a)iro.umontreal.xn--ca-02t at 2022-04-03T06:11:39+00:00 location -> sinfo - - - - - 12 changed files: - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/eval.ml - src/heap.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/positivity.ml - src/sexp.ml - src/unification.ml Changes: ===================================== src/REPL.ml ===================================== @@ -136,7 +136,7 @@ let eval_interactive let ldecls, ectx' = Elab.lexp_p_decls decls [] ectx in let lexprs = Elab.lexp_parse_all exprs ectx' in - List.iter (fun lexpr -> ignore (OL.check (ectx_to_lctx ectx') lexpr dummy_sinfo)) lexprs; + List.iter (fun lexpr -> ignore (OL.check (ectx_to_lctx ectx') lexpr)) lexprs; List.iter interactive#process_decls ldecls; Log.print_log (); ===================================== src/builtin.ml ===================================== @@ -90,7 +90,7 @@ let predef_map : lexp SMap.t ref let get_predef (name: string) (ctx: DB.elab_context) : lexp = try let r = (DB.get_size ctx) - !builtin_size - 0 in let p = SMap.find name (!predef_map) in - mkSusp p (S.shift r) dummy_sinfo + mkSusp p (S.shift r) with Not_found -> log_raise_error {|"%s" was not predefined|} name let set_predef name lexp @@ -100,7 +100,7 @@ let set_predef name lexp let dloc = DB.dloc let op_binary t = mkArrow (Anormal, (dloc, None), t, dloc, - mkArrow (Anormal, (dloc, None), t, dloc, t) dummy_sinfo) dummy_sinfo + mkArrow (Anormal, (dloc, None), t, dloc, t) ) let o2l_bool ctx b = get_predef (if b then "true" else "false") ctx @@ -136,11 +136,11 @@ let lmap = ref (SMap.empty : (lexp * ltype) SMap.t) let add_builtin_cst (name : string) (e : lexp) = let map = !lmap in assert (not (SMap.mem name map)); - let t = OL.check Myers.nil e dummy_sinfo in + let t = OL.check Myers.nil e in lmap := SMap.add name (e, t) map let new_builtin_type name kind = - let t = mkBuiltin ((dloc, name), kind) dummy_sinfo in + let t = mkBuiltin ((dloc, name), kind) in add_builtin_cst name t; t @@ -159,7 +159,7 @@ let register_builtin_csts () = add_builtin_cst "Eq.refl" DB.eq_refl let type_arrow_0 = - mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0) dummy_sinfo + mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0) let register_builtin_types () = let _ = new_builtin_type "Sexp" DB.type0 in ===================================== src/debruijn.ml ===================================== @@ -84,34 +84,34 @@ let fatal ?print_action ?loc fmt = * ---------------------------------- *) let dloc = dummy_location -let type_level_sort = mkSort (dloc, StypeLevel) dummy_sinfo -let sort_omega = mkSort (dloc, StypeOmega) dummy_sinfo -let type_level = mkBuiltin ((dloc, "TypeLevel"), type_level_sort) dummy_sinfo -let level0 = mkSortLevel SLz dummy_sinfo -let level1 = mkSortLevel (mkSLsucc level0) dummy_sinfo -let level2 = mkSortLevel (mkSLsucc level1) dummy_sinfo -let type0 = mkSort (dloc, Stype level0) dummy_sinfo -let type1 = mkSort (dloc, Stype level1) dummy_sinfo -let type2 = mkSort (dloc, Stype level2) dummy_sinfo -let type_int = mkBuiltin ((dloc, "Int"), type0) dummy_sinfo -let type_integer = mkBuiltin ((dloc, "Integer"), type0) dummy_sinfo -let type_float = mkBuiltin ((dloc, "Float"), type0) dummy_sinfo -let type_string = mkBuiltin ((dloc, "String"), type0) dummy_sinfo -let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0) dummy_sinfo +let type_level_sort = mkSort (dloc, StypeLevel) +let sort_omega = mkSort (dloc, StypeOmega) +let type_level = mkBuiltin ((dloc, "TypeLevel"), type_level_sort) +let level0 = mkSortLevel SLz +let level1 = mkSortLevel (mkSLsucc level0) +let level2 = mkSortLevel (mkSLsucc level1) +let type0 = mkSort (dloc, Stype level0) +let type1 = mkSort (dloc, Stype level1) +let type2 = mkSort (dloc, Stype level2) +let type_int = mkBuiltin ((dloc, "Int"), type0) +let type_integer = mkBuiltin ((dloc, "Integer"), type0) +let type_float = mkBuiltin ((dloc, "Float"), type0) +let type_string = mkBuiltin ((dloc, "String"), type0) +let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0) let type_eq_type = let lv = (dloc, Some "l") in let tv = (dloc, Some "t") in mkArrow (Aerasable, lv, type_level, dloc, mkArrow (Aerasable, tv, - mkSort (dloc, Stype (mkVar (lv, 0) dummy_sinfo)) dummy_sinfo , dloc, + mkSort (dloc, Stype (mkVar (lv, 0))) , dloc, mkArrow (Anormal, (dloc, None), - mkVar (tv, 0) dummy_sinfo, dloc, + mkVar (tv, 0), dloc, mkArrow (Anormal, (dloc, None), - mkVar (tv, 1) dummy_sinfo, dloc, - mkSort (dloc, Stype (mkVar (lv, 3) dummy_sinfo)) dummy_sinfo) dummy_sinfo) dummy_sinfo) dummy_sinfo) + mkVar (tv, 1) , dloc, + mkSort (dloc, Stype (mkVar (lv, 3))))))) -let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type dummy_sinfo) dummy_sinfo +let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) let eq_refl = let lv = (dloc, Some "l") in @@ -121,14 +121,14 @@ let eq_refl = mkArrow (Aerasable, lv, type_level, dloc, mkArrow (Aerasable, tv, - mkSort (dloc, Stype (mkVar (lv, 0) dummy_sinfo)) dummy_sinfo, dloc, + mkSort (dloc, Stype (mkVar (lv, 0))), dloc, mkArrow (Aerasable, xv, - mkVar (tv, 0) dummy_sinfo, dloc, + mkVar (tv, 0), dloc, mkCall (type_eq, - [Aerasable, mkVar (lv, 2) dummy_sinfo; - Aerasable, mkVar (tv, 1) dummy_sinfo; - Anormal, mkVar (xv, 0) dummy_sinfo; - Anormal, mkVar (xv, 0) dummy_sinfo]) dummy_sinfo) dummy_sinfo) dummy_sinfo) dummy_sinfo) dummy_sinfo + [Aerasable, mkVar (lv, 2); + Aerasable, mkVar (tv, 1); + Anormal, mkVar (xv, 0); + Anormal, mkVar (xv, 0)]))))) (* easier to debug with type annotations *) @@ -296,7 +296,7 @@ let print_lexp_ctx_n (ctx : lexp_context) (ranges : (int * int) list) = (match lexp with | None -> print_string "<var>" | Some lexp - -> (let str = lexp_str (!debug_ppctx) lexp dummy_sinfo in + -> (let str = lexp_str (!debug_ppctx) lexp in let strs = match String.split_on_char '\n' str with | hd :: tl -> print_string hd; tl @@ -383,12 +383,12 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = let lctx_lookup_type (ctx : lexp_context) (vref : vref) : lexp = let (_, i) = vref in let (_, _, t) = lctx_lookup ctx vref in - mkSusp t (S.shift (i + 1)) dummy_sinfo + mkSusp t (S.shift (i + 1)) let lctx_lookup_value (ctx : lexp_context) (vref : vref) : lexp option = let (_, i) = vref in match lctx_lookup ctx vref with - | (_, LetDef (o, v), _) -> Some (push_susp v (S.shift (i + 1 - o)) dummy_sinfo) + | (_, LetDef (o, v), _) -> Some (push_susp v (S.shift (i + 1 - o))) | _ -> None let env_lookup_type ctx (v : vref): lexp = ===================================== src/elab.ml ===================================== @@ -111,7 +111,7 @@ let special_forms : special_forms_map ref = ref SMap.empty let type_special_form = BI.new_builtin_type "Special-Form" type0 let add_special_form (name, func) = - BI.add_builtin_cst name (mkBuiltin ((dloc, name) , type_special_form) dummy_sinfo); + BI.add_builtin_cst name (mkBuiltin ((dloc, name) , type_special_form)); special_forms := SMap.add name func (!special_forms) let get_special_form name = @@ -141,7 +141,7 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = -> lexp_error l ltp {|Type of "%s" is not a proper type: %s|} name tystr let elab_check_proper_type (ctx : elab_context) ltp var = - try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp dummy_sinfo) var ltp + try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) var ltp with e -> match e with | Log.Stop_compilation _ -> raise e | _ @@ -161,7 +161,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in let loc = lexp_location lxp in - let ltype' = try OL.check lctx lxp dummy_sinfo + let ltype' = try OL.check lctx lxp with e -> match e with | Log.Stop_compilation _ -> raise e | _ -> @@ -210,13 +210,13 @@ let ctx_define_rec (ctx: elab_context) decls = let nctx = ectx_extend_rec ctx decls in let _ = List.fold_left (fun n (var, _lxp, ltp) -> elab_check_proper_type - nctx (push_susp ltp (S.shift n) dummy_sinfo) var; + nctx (push_susp ltp (S.shift n)) var; n - 1) (List.length decls) decls in let _ = List.fold_left (fun n (var, lxp, ltp) -> elab_check_def nctx var lxp - (push_susp ltp (S.shift n) dummy_sinfo); + (push_susp ltp (S.shift n)); n - 1) (List.length decls) decls in @@ -261,14 +261,14 @@ let ctx_define_rec (ctx: elab_context) decls = let newMetavar (ctx : lexp_context) sl name t = let meta = Unif.create_metavar ctx sl t in - mkMetavar (meta, S.identity, name) dummy_sinfo + mkMetavar (meta, S.identity, name) let newMetalevel (ctx : lexp_context) sl loc = newMetavar ctx sl (loc, Some "ℓ") type_level let newMetatype (ctx : lexp_context) sl loc = newMetavar ctx sl (loc, Some "τ") - (mkSort (loc, Stype (newMetalevel ctx sl loc)) dummy_sinfo) + (mkSort (loc, Stype (newMetalevel ctx sl loc))) (* Functions used when we need to return some lexp/ltype but * an error makes it impossible to return "the right one". *) @@ -303,7 +303,7 @@ let elab_varref ctx (loc, name) = try let idx = senv_lookup name ctx in let id = (loc, Some name) in - let lxp = mkVar (id, idx) dummy_sinfo in + let lxp = mkVar (id, idx) in let ltp = env_lookup_type ctx (id, idx) in (lxp, Inferred ltp) with Senv_Lookup_Fail xs -> @@ -317,7 +317,7 @@ let elab_varref ctx (loc, name) (* Turn metavar into plain vars after generalization. * ids: an IMap that maps metavars to their position as argument * (first arg gets position 0). *) -let meta_to_var ids (e : lexp) sinfo = +let meta_to_var ids (e : lexp) = let count = IMap.cardinal ids in @@ -423,13 +423,13 @@ let meta_to_var ids (e : lexp) sinfo = match lexp_lexp' e with | Imm _ -> e | SortLevel SLz -> e - | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (loop o e)) sinfo - | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (loop o e1, loop o e2)) sinfo - | Sort (l, Stype e) -> mkSort (l, Stype (loop o e)) sinfo + | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (loop o e)) + | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (loop o e1, loop o e2)) + | Sort (l, Stype e) -> mkSort (l, Stype (loop o e)) | Sort (_, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e - | Var (n,i) -> if i < o then e else mkVar (n, i + count) sinfo - | Susp (e, s) -> loop o (push_susp e s dummy_sinfo) + | Var (n,i) -> if i < o then e else mkVar (n, i + count) + | Susp (e, s) -> loop o (push_susp e s) | Let (l, defs, e) -> let len = List.length defs in let (_, ndefs) @@ -438,13 +438,13 @@ let meta_to_var ids (e : lexp) sinfo = (o', (l, loop (len + o) e, loop (o' + o) t) :: defs)) defs (len, []) in - mkLet (l, ndefs, loop (len + o) e) sinfo + mkLet (l, ndefs, loop (len + o) e) | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, loop o t1, l, loop (1 + o) t2) sinfo + -> mkArrow (ak, v, loop o t1, l, loop (1 + o) t2) | Lambda (ak, v, t, e) - -> mkLambda (ak, v, loop o t, loop (1 + o) e) sinfo + -> mkLambda (ak, v, loop o t, loop (1 + o) e) | Call (f, args) - -> mkCall (loop o f, List.map (fun (ak, e) -> (ak, loop o e)) args) sinfo + -> mkCall (loop o f, List.map (fun (ak, e) -> (ak, loop o e)) args) | Inductive (l, label, args, cases) -> let alen = List.length args in let (_, nargs) @@ -466,8 +466,8 @@ let meta_to_var ids (e : lexp) sinfo = fields (flen + alen, []) in nfields) cases in - mkInductive (l, label, nargs, ncases) sinfo - | Cons (t, l) -> mkCons (loop o t, l) sinfo + mkInductive (l, label, nargs, ncases) + | Cons (t, l) -> mkCons (loop o t, l) | Case (l, e, t, cases, default) -> let ncases = SMap.map @@ -476,13 +476,13 @@ let meta_to_var ids (e : lexp) sinfo = cases in mkCase (l, loop o e, loop o t, ncases, match default with None -> None - | Some (v, e) -> Some (v, loop (2 + o) e)) sinfo + | Some (v, e) -> Some (v, loop (2 + o) e)) | Metavar (id, s, name) -> if IMap.mem id ids then - mkVar (name, o + count - IMap.find id ids) sinfo + mkVar (name, o + count - IMap.find id ids) else match metavar_lookup id with - | MVal e -> loop o (push_susp e s dummy_sinfo) - | _ -> mkMetavar (id, adjust_subst o s, name) sinfo + | MVal e -> loop o (push_susp e s) + | _ -> mkMetavar (id, adjust_subst o s, name) in loop 0 e let sort_generalized_metavars sl cl ctx mfvs = @@ -503,7 +503,7 @@ let sort_generalized_metavars sl cl ctx mfvs = then acc else (assert (cl' >= cl); let mt = if cl' > cl then - Inverse_subst.apply_inv_subst mt (S.shift (cl' - cl)) dummy_sinfo + Inverse_subst.apply_inv_subst mt (S.shift (cl' - cl)) else mt in let mv = (id, vname, mt) in if (OL.conv_p ctx mt type_level) then @@ -536,9 +536,9 @@ let generalize (nctx : elab_context) e = assert (n = IMap.cardinal ids); match mfvs with | [] -> assert (n = len); - meta_to_var ids e dummy_sinfo + meta_to_var ids e | ((id, vname, mt) :: mfvs) - -> let mt' = meta_to_var ids mt dummy_sinfo in + -> let mt' = meta_to_var ids mt in let n = n + 1 in let e' = loop (IMap.add id n ids) n mfvs in wrap (IMap.mem id nes) vname mt' l e' in @@ -621,11 +621,11 @@ and instantiate_implicit e t ctx = match OL.lexp'_whnf t (ectx_to_lctx ctx) with | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) -> let arg = get_implicit_arg ctx (lexp_location e) v t1 in - instantiate (mkSusp t2 (S.substitute arg) dummy_sinfo) ((ak, arg)::args) - | _ -> (mkCall (e, List.rev args) dummy_sinfo, t) + instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) + | _ -> (mkCall (e, List.rev args), t) in instantiate t [] -and infer_type pexp ectx var sinfo = +and infer_type pexp ectx var = (* We could also use lexp_check with an argument of the form * Sort (?s), but in most cases the metavar would be allocated * unnecessarily. *) @@ -643,7 +643,7 @@ and infer_type pexp ectx var sinfo = Unif.unify (mkSort (l, Stype (newMetalevel (ectx_to_lctx ectx) (ectx_to_scope_level ectx) - l)) sinfo) + l))) s (ectx_to_lctx ectx) with | (_::_) @@ -658,7 +658,7 @@ and infer_type pexp ectx var sinfo = t and lexp_let_decls declss (body: lexp) _ctx = - List.fold_right (fun decls lxp -> mkLet (dloc, decls, lxp) dummy_sinfo) + List.fold_right (fun decls lxp -> mkLet (dloc, decls, lxp)) declss body and unify_with_arrow ctx tloc lxp kind var aty @@ -668,7 +668,7 @@ and unify_with_arrow ctx tloc lxp kind var aty let nctx = ectx_extend ctx var Variable arg in let body = newMetatype (ectx_to_lctx nctx) (ectx_to_scope_level ctx) tloc in let (l, _) = var in - let arrow = mkArrow (kind, var, arg, l, body) dummy_sinfo in + let arrow = mkArrow (kind, var, arg, l, body) in match Unif.unify arrow lxp (ectx_to_lctx ctx) with | ((_ck, _ctx, t1, t2)::_) -> lexp_error @@ -756,12 +756,12 @@ and check_case rtype (loc, target, ppatterns) ctx = -> let arg = newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) - name (mkSusp t s dummy_sinfo) in + name (mkSusp t s) in (S.cons arg s, (ak, arg) :: targs)) (S.identity, []) fargs in let (cs, args) = (constructors, List.rev targs) in - ltarget := check_inferred ctx tlxp tltp (mkCall (it', args) dummy_sinfo); + ltarget := check_inferred ctx tlxp tltp (mkCall (it', args)); it_cs_as := Some (it', cs, args); (cs, args) | _ -> let call_split e = @@ -788,7 +788,7 @@ and check_case rtype (loc, target, ppatterns) ctx = let shift_to_extended_ctx nctx lexp = mkSusp lexp (S.shift (M.length (ectx_to_lctx nctx) - - M.length (ectx_to_lctx ctx))) dummy_sinfo in + - M.length (ectx_to_lctx ctx))) in let ctx_extend_with_eq nctx head_lexp = (* Add a proof of equality between the target and the branch @@ -800,14 +800,14 @@ and check_case rtype (loc, target, ppatterns) ctx = [(Aerasable, tlvl'); (* Typelevel *) (Aerasable, tltp'); (* Inductive type *) (Anormal, head_lexp); (* Lexp of the branch head *) - (Anormal, tlxp')]) dummy_sinfo (* Target lexp *) + (Anormal, tlxp')]) (* Target lexp *) in ctx_extend nctx (loc, None) Variable eqty in let add_default v = (if dflt != None then uniqueness_warn pat); let nctx = ctx_extend ctx v Variable tltp in - let head_lexp = mkVar (v, 0) dummy_sinfo in + let head_lexp = mkVar (v, 0) in let nctx = ctx_extend_with_eq nctx head_lexp in let rtype' = shift_to_extended_ctx nctx rtype in let lexp = check pexp rtype' nctx in @@ -824,7 +824,7 @@ and check_case rtype (loc, target, ppatterns) ctx = v t in let nctx = ctx_extend ctx v Variable t in let body = inst_args nctx body in - mkSusp body (S.substitute arg) dummy_sinfo + mkSusp body (S.substitute arg) | _e -> lxp in match lexp_lexp' (nosusp (inst_args ctx lctor)) with | Cons (it', (_, cons_name)) @@ -861,16 +861,16 @@ and check_case rtype (loc, target, ppatterns) ctx = | (_, (ak, (_, Some fname), fty)::cargs) when SMap.mem fname pe -> let var = SMap.find fname pe in - let nctx = ctx_extend ctx var Variable (mkSusp fty s dummy_sinfo) in - make_nctx nctx (ssink dummy_sinfo var s) pargs cargs + let nctx = ctx_extend ctx var Variable (mkSusp fty s) in + make_nctx nctx (ssink var s) pargs cargs (SMap.remove fname pe) ((ak, var)::acc) | ((ef, var)::pargs, (ak, _, fty)::cargs) when (match (ef, ak) with | (Some (_, "_"), _) | (None, Anormal) -> true | _ -> false) - -> let nctx = ctx_extend ctx var Variable (mkSusp fty s dummy_sinfo) in - make_nctx nctx (ssink dummy_sinfo var s) pargs cargs pe + -> let nctx = ctx_extend ctx var Variable (mkSusp fty s) in + make_nctx nctx (ssink var s) pargs cargs pe ((ak, var)::acc) | ((Some (l, fname), var)::pargs, cargs) -> if SMap.mem fname pe then @@ -878,23 +878,23 @@ and check_case rtype (loc, target, ppatterns) ctx = make_nctx ctx s pargs cargs (SMap.add fname var pe) acc | pargs, (ak, fname, fty)::cargs -> let var = (loc, None) in - let nctx = ctx_extend ctx var Variable (mkSusp fty s dummy_sinfo) in + let nctx = ctx_extend ctx var Variable (mkSusp fty s) in if ak = Anormal then sexp_error loc {|Missing pattern for normal field%s|} (match fname with | (_, Some n) -> sprintf {| "%s"|} n | _ -> ""); - make_nctx nctx (ssink dummy_sinfo var s) pargs cargs pe + make_nctx nctx (ssink var s) pargs cargs pe ((ak, var)::acc) in let nctx, fargs = make_nctx ctx subst pargs cargs SMap.empty [] in let head_lexp_ctor = shift_to_extended_ctx nctx - (mkCall (lctor, List.map (fun (_, a) -> (Aerasable, a)) targs) dummy_sinfo) in + (mkCall (lctor, List.map (fun (_, a) -> (Aerasable, a)) targs)) in let head_lexp_args = List.mapi (fun i (ak, vname) -> - (ak, mkVar (vname, List.length fargs - i - 1) dummy_sinfo)) fargs in - let head_lexp = mkCall (head_lexp_ctor, head_lexp_args) dummy_sinfo in + (ak, mkVar (vname, List.length fargs - i - 1))) fargs in + let head_lexp = mkCall (head_lexp_ctor, head_lexp_args) in let nctx = ctx_extend_with_eq nctx head_lexp in let rtype' = shift_to_extended_ctx nctx rtype in let lexp = check pexp rtype' nctx in @@ -908,7 +908,7 @@ and check_case rtype (loc, target, ppatterns) ctx = match pat with | Ppatsym ((_, None) as var) -> add_default var | Ppatsym ((l, Some name) as var) - -> if Eval.constructor_p name ctx dummy_sinfo then + -> if Eval.constructor_p name ctx then add_branch (Symbol (l, name)) [] else add_default var (* A named default branch. *) @@ -917,7 +917,7 @@ and check_case rtype (loc, target, ppatterns) ctx = let (lpattern, dflt) = List.fold_left fold_fun (SMap.empty, None) ppatterns in - mkCase (loc, tlxp, rtype, lpattern, dflt) dummy_sinfo + mkCase (loc, tlxp, rtype, lpattern, dflt) and elab_macro_call ctx func args ot = let t @@ -926,7 +926,7 @@ and elab_macro_call ctx func args ot = (lexp_location func) | Some t -> t in let sxp = match lexp_expand_macro (lexp_location func) - func args ctx (Some t) dummy_sinfo with + func args ctx (Some t) with | Vcommand cmd -> (match cmd () with | Vsexp (sxp) -> sxp @@ -949,7 +949,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = let larg = check sarg arg_type ctx in handle_fun_args ((ak, larg) :: largs) sargs (SMap.remove aname pending) - (L.mkSusp ret_type (S.substitute larg) dummy_sinfo) + (L.mkSusp ret_type (S.substitute larg)) | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs, Arrow (ak, _, arg_type, _, ret_type) @@ -957,7 +957,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = (* Explicit-implicit argument. *) -> let larg = check sarg arg_type ctx in handle_fun_args ((ak, larg) :: largs) sargs pending - (L.mkSusp ret_type (S.substitute larg) dummy_sinfo) + (L.mkSusp ret_type (S.substitute larg)) | (Node (Symbol (_, "_:=_"), [Symbol (l, aname); sarg])) :: sargs, Arrow _ @@ -982,7 +982,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = | sarg::_ -> sexp_location sarg) v arg_type in handle_fun_args ((ak, larg) :: largs) sargs pending - (L.mkSusp ret_type (S.substitute larg) dummy_sinfo) + (L.mkSusp ret_type (S.substitute larg)) | [], _ -> (if not (SMap.is_empty pending) then let pending = SMap.bindings pending in @@ -1002,10 +1002,10 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = ltp' Anormal (dloc, None) None in let larg = check sarg arg_type ctx in handle_fun_args ((Anormal, larg) :: largs) sargs pending - (L.mkSusp ret_type (S.substitute larg) dummy_sinfo) in + (L.mkSusp ret_type (S.substitute larg)) in let (largs, ret_type) = handle_fun_args [] sargs SMap.empty ltp in - (mkCall (func, List.rev largs) dummy_sinfo, Inferred ret_type) + (mkCall (func, List.rev largs), Inferred ret_type) (* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx = @@ -1022,11 +1022,11 @@ and lexp_parse_inductive ctors ctx = * things like `fv` and `meta_to_var`. *) let altacc = List.fold_right (fun (ak, n, t) aa - -> mkArrow (ak, n, t, dummy_location, aa) dummy_sinfo) + -> mkArrow (ak, n, t, dummy_location, aa)) acc impossible in let g = generalize nctx altacc in let altacc' = g (fun _ne vname t l e - -> mkArrow (Aerasable, vname, t, l, e) dummy_sinfo) + -> mkArrow (Aerasable, vname, t, l, e)) altacc in if altacc' == altacc then acc (* No generalization! *) @@ -1038,7 +1038,7 @@ and lexp_parse_inductive ctors ctx = | _ -> assert (e = impossible); [] in loop altacc' | (kind, var, exp)::tl - -> let lxp = infer_type exp ctx var dummy_sinfo in + -> let lxp = infer_type exp ctx var in let nctx = ectx_extend ctx var Variable lxp in loop tl ((kind, var, lxp)::acc) nctx in loop args [] nctx in @@ -1089,16 +1089,16 @@ and lexp_eval ectx e = "Exception happened during evaluation:"; raise exc -and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) sinfo +and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) : value_type = (* Build the function to be called *) let macro_expand = BI.get_predef "Macro_expand" ctx in (* FIXME: Rather than remember the lexp of "expand_macro" in predef, * we should remember its value so we don't have to re-eval it everytime. *) - let macro_expand = lexp_eval ctx macro_expand sinfo in + let macro_expand = lexp_eval ctx macro_expand in (* FIXME: provide `ot` (the optional expected type) for non-decl macros. *) - let macro = lexp_eval ctx macro_funct sinfo in + let macro = lexp_eval ctx macro_funct in let args = [macro; BI.o2v_list sargs] in (* FIXME: Make a proper `Var`. *) @@ -1116,7 +1116,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: sexp = try let lxp, _ltp = infer (Symbol (loc, mname)) ctx in (* FIXME: Check that (conv_p ltp Macro)! *) - let ret = lexp_expand_macro loc lxp sargs ctx None dummy_sinfo in + let ret = lexp_expand_macro loc lxp sargs ctx None in match ret with | Vcommand cmd -> (match cmd () with @@ -1149,7 +1149,7 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) assert (i < List.length defs); match Myers.nth i (ectx_to_lctx nctx) with | (_v', ForwardRef, t) - -> let adjusted_t = push_susp t (S.shift (i + 1)) dummy_sinfo in + -> let adjusted_t = push_susp t (S.shift (i + 1)) in (* We elab `sexp` within the original `nctx`, i.e. * the context where the other vars don't have * a definition yet. This is because we can't yet @@ -1164,9 +1164,9 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in decls, ctx_define_rec ectx decls -and infer_and_generalize_type (ctx : elab_context) se name sinfo = +and infer_and_generalize_type (ctx : elab_context) se name = let nctx = ectx_new_scope ctx in - let t = infer_type se nctx name sinfo in + let t = infer_type se nctx name in (* We should not generalize over metavars which only occur on the rightmost * side of arrows in type annotations (aka declarations), since there's no * way for the callee to return something of the proper type if those @@ -1193,12 +1193,12 @@ and infer_and_generalize_type (ctx : elab_context) se name sinfo = let rec strip_rettype t = match lexp_lexp' t with | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, t1, l, strip_rettype t2) sinfo + -> mkArrow (ak, v, t1, l, strip_rettype t2) | Sort _ | Metavar _ -> type0 (* Abritrary closed constant. *) | _ -> t in let g = generalize nctx (strip_rettype t) in g (fun _ne name t l e - -> mkArrow (Aerasable, name, t, l, e) sinfo) + -> mkArrow (Aerasable, name, t, l, e)) t and infer_and_generalize_def (ctx : elab_context) se = @@ -1207,11 +1207,11 @@ and infer_and_generalize_def (ctx : elab_context) se = let g = generalize nctx e in let e' = g (fun ne vname t _l e -> mkLambda ((if ne then Aimplicit else Aerasable), - vname, t, e) dummy_sinfo) + vname, t, e)) e in let t' = g (fun ne name t _l e -> mkArrow ((if ne then Aimplicit else Aerasable), - name, t, sexp_location se, e) dummy_sinfo) + name, t, sexp_location se, e)) t in (e', t') @@ -1255,13 +1255,13 @@ and lexp_decls_1 (* FIXME: Move this to a "special form"! *) -> (match args with | [Symbol (loc, vname); stp] - -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) dummy_sinfo in + -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) in if SMap.mem vname pending_decls then (* Don't burp: take'em all and unify! *) let pt_idx = senv_lookup vname nctx in (* Take the previous type annotation. *) let pt = match Myers.nth pt_idx (ectx_to_lctx nctx) with - | (_, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) dummy_sinfo + | (_, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) | _ -> Log.internal_error "Var not found at its index!" in (* Unify it with the new one. *) let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with @@ -1297,7 +1297,7 @@ and lexp_decls_1 let var = (l, Some vname) in (* Lexp decls are always recursive, so we have to shift by 1 to * account for the extra var (ourselves). *) - [(var, mkSusp lexp (S.shift 1) dummy_sinfo, ltp)], sdecls, toks, + [(var, mkSusp lexp (S.shift 1), ltp)], sdecls, toks, ctx_define nctx var lexp ltp | [Symbol (loc, vname); sexp] @@ -1408,8 +1408,8 @@ let sform_built_in ctx loc sargs ot = * function. It's not indispensible, tho it might still be useful for * performance of type-inference (at least until we have proper * memoization of push_susp and/or whnf). *) - -> let ltp' = L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) dummy_sinfo in - let bi = mkBuiltin ((loc, name), ltp') dummy_sinfo in + -> let ltp' = L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) in + let bi = mkBuiltin ((loc, name), ltp') in if not (SMap.mem name (!EV.builtin_functions)) then sexp_error loc {|Unknown built-in "%s"|} name; BI.add_builtin_cst name bi; @@ -1427,7 +1427,7 @@ let sform_datacons ctx loc sargs _ot = match sargs with | [t; Symbol ((_sloc, _cname) as sym)] -> let idt, _ = infer t ctx in - (mkCons (idt, sym) dummy_sinfo, Lazy) + (mkCons (idt, sym), Lazy) | [_;_] -> sexp_error loc "Second arg of ##constr should be a symbol"; sform_dummy_ret ctx loc @@ -1499,11 +1499,11 @@ let sform_typecons ctx loc sargs _ot = constrs [] in let map_ctor = lexp_parse_inductive ctors nctx in - (mkInductive (loc, label, formals, map_ctor) dummy_sinfo, Lazy) + (mkInductive (loc, label, formals, map_ctor), Lazy) let sform_hastype ctx loc sargs _ot = match sargs with - | [se; st] -> let lt = infer_type st ctx (loc, None) dummy_sinfo in + | [se; st] -> let lt = infer_type st ctx (loc, None) in let le = check se lt ctx in (le, Inferred lt) | _ -> sexp_error loc "##_:_ takes two arguments"; @@ -1515,18 +1515,18 @@ let sform_arrow kind ctx loc sargs _ot = -> let (v, st1) = match st1 with | Node (Symbol (_, "_:_"), [Symbol v; st1]) -> (elab_p_id v, st1) | _ -> ((sexp_location st1, None), st1) in - let lt1 = infer_type st1 ctx v dummy_sinfo in + let lt1 = infer_type st1 ctx v in let nctx = ectx_extend ctx v Variable lt1 in - let lt2 = infer_type st2 nctx (sexp_location st2, None) dummy_sinfo in - (mkArrow (kind, v, lt1, loc, lt2) dummy_sinfo, Lazy) + let lt2 = infer_type st2 nctx (sexp_location st2, None) in + (mkArrow (kind, v, lt1, loc, lt2), Lazy) | _ -> sexp_error loc "##_->_ takes two arguments"; sform_dummy_ret ctx loc let sform_immediate ctx loc sargs ot = match sargs with - | [(String _) as se] -> mkImm (se) dummy_sinfo, Inferred DB.type_string - | [(Integer _) as se] -> mkImm (se) dummy_sinfo, Inferred DB.type_int - | [(Float _) as se] -> mkImm (se) dummy_sinfo, Inferred DB.type_float + | [(String _) as se] -> mkImm (se), Inferred DB.type_string + | [(Integer _) as se] -> mkImm (se), Inferred DB.type_int + | [(Float _) as se] -> mkImm (se), Inferred DB.type_float | [Block (_location, pts)] -> let grm = ectx_get_grammar ctx in let tokens = lex default_stt pts in @@ -1575,7 +1575,7 @@ let sform_identifier ctx loc sargs ot = match (metavar_lookup idx) with | MVar (sl',_,_) -> if sl = sl' then - (mkMetavar (idx, subst, (loc, Some name)) dummy_sinfo, Lazy) + (mkMetavar (idx, subst, (loc, Some name)), Lazy) else (* FIXME: The variable is from another scope_level! It means that `subst` is not the right substitution for @@ -1592,7 +1592,7 @@ let sform_identifier ctx loc sargs ot = | None -> newMetatype octx sl loc | Some t (* `t` is defined in ctx instead of octx. *) - -> Inverse_subst.apply_inv_subst t subst dummy_sinfo in + -> Inverse_subst.apply_inv_subst t subst in let mv = newMetavar octx sl (loc, Some name) t in (if not (name = "") then let idx = @@ -1600,7 +1600,7 @@ let sform_identifier ctx loc sargs ot = | Metavar (idx, _, _) -> idx | _ -> fatal ~loc "newMetavar returned a non-Metavar" in rmmap := SMap.add name idx (!rmmap)); - (mkSusp mv subst dummy_sinfo, + (mkSusp mv subst, match ot with Some _ -> Checked | None -> Lazy) (* Normal identifier. *) @@ -1625,7 +1625,7 @@ let rec sform_lambda kind ctx loc sargs ot = ((dummy_location, None), None) in let olt1 = match ost1 with - | Some st -> Some (infer_type st ctx arg dummy_sinfo) + | Some st -> Some (infer_type st ctx arg) | _ -> None in let mklam lt1 olt2 = @@ -1638,9 +1638,9 @@ let rec sform_lambda kind ctx loc sargs ot = | Some lt2 -> Some (srename arg lt2) in let (lbody, alt) = elaborate nctx sbody olt2 in - (mkLambda (kind, arg, lt1, lbody) dummy_sinfo, + (mkLambda (kind, arg, lt1, lbody), match alt with - | Inferred lt2 -> Inferred (mkArrow (kind, arg, lt1, loc, lt2) dummy_sinfo) + | Inferred lt2 -> Inferred (mkArrow (kind, arg, lt1, loc, lt2)) | _ -> alt) in (match ot with @@ -1672,9 +1672,9 @@ let rec sform_lambda kind ctx loc sargs ot = (* FIXME: Don't go back to sform_lambda, but use an internal * loop to avoid re-computing olt1 each time. *) let (lam, alt) = sform_lambda kind nctx loc sargs (Some lt2) in - (mkLambda (ak2, v, lt1, lam) dummy_sinfo, + (mkLambda (ak2, v, lt1, lam), match alt with - | Inferred lt2' -> Inferred (mkArrow (ak2, v, lt1, loc, lt2') dummy_sinfo) + | Inferred lt2' -> Inferred (mkArrow (ak2, v, lt1, loc, lt2')) | _ -> alt) | _lt @@ -1717,10 +1717,10 @@ let sform_letin ctx loc sargs ot = match sargs with List.fold_left (fun (s, off) decls -> (OL.lexp_defs_subst loc s decls, off + List.length decls)) (S.identity, 0) declss in - let ot = Option.map (fun t -> mkSusp t (S.shift off) dummy_sinfo) ot in + let ot = Option.map (fun t -> mkSusp t (S.shift off)) ot in let bdy, ot = elaborate nctx sbody ot in let ot = match ot with - | Inferred t -> Inferred (mkSusp t s dummy_sinfo) + | Inferred t -> Inferred (mkSusp t s) | _ -> ot in (lexp_let_decls declss bdy nctx, ot) | _ -> sexp_error loc "Unrecognized let_in_ expression"; @@ -1728,10 +1728,10 @@ let sform_letin ctx loc sargs ot = match sargs with let rec infer_level ctx se : lexp = match se with - | Symbol (_, "z") -> mkSortLevel SLz dummy_sinfo + | Symbol (_, "z") -> mkSortLevel SLz | Symbol _ -> check se type_level ctx | Node (Symbol (_, "s"), [se]) - -> mkSortLevel (SLsucc (infer_level ctx se)) dummy_sinfo + -> mkSortLevel (SLsucc (infer_level ctx se)) | Node (Symbol (_, "_∪_"), [se1; se2]) -> OL.mkSLlub (ectx_to_lctx ctx) (infer_level ctx se1) (infer_level ctx se2) | _ -> let l = (sexp_location se) in @@ -1747,8 +1747,8 @@ let rec infer_level ctx se : lexp = let sform_type ctx loc sargs _ot = match sargs with | [se] -> let l = infer_level ctx se in - (mkSort (loc, Stype l) dummy_sinfo, - Inferred (mkSort (loc, Stype (mkSortLevel (mkSLsucc l) dummy_sinfo)) dummy_sinfo)) + (mkSort (loc, Stype l), + Inferred (mkSort (loc, Stype (mkSortLevel (mkSLsucc l))))) | _ -> (sexp_error loc "##Type_ expects one argument"; sform_dummy_ret ctx loc) @@ -1759,7 +1759,7 @@ let sform_debruijn ctx loc sargs _ot = (sexp_error l "##DeBruijn index out of bounds"; sform_dummy_ret ctx loc) else - let lxp = mkVar ((loc, None), i) dummy_sinfo in (lxp, Lazy) + let lxp = mkVar ((loc, None), i) in (lxp, Lazy) | _ -> (sexp_error loc "##DeBruijn expects one integer argument"; sform_dummy_ret ctx loc) @@ -1831,7 +1831,7 @@ let sform_load usr_elctx loc sargs _ot = let tuple' = if !in_pervasive then tuple else - (Lexp.mkSusp tuple (S.shift (usr_len - dflt_len)) dummy_sinfo) in + (Lexp.mkSusp tuple (S.shift (usr_len - dflt_len))) in (tuple',Lazy) @@ -1890,7 +1890,7 @@ let default_ectx let register_predefs elctx = try List.iter (fun name -> let idx = senv_lookup name elctx in - let v = mkVar ((dloc, Some name), idx) dummy_sinfo in + let v = mkVar ((dloc, Some name), idx) in BI.set_predef name v) BI.predef_names; with Senv_Lookup_Fail _ -> warning "Predef not found"; in @@ -1939,7 +1939,7 @@ let lexp_expr_str str ctx = let source = new Source.source_string str in let pxps = sexp_parse_source source tenv grm limit in let lexps = lexp_parse_all pxps ctx in - List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp dummy_sinfo)) + List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp)) lexps; lexps ===================================== src/eval.ml ===================================== @@ -421,7 +421,7 @@ let file_write loc _depth args_val = match args_val with ) "File.write expects an out_channel and a string. Actual arguments:" -let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info) sinfo : (value_type) = +let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info) : (value_type) = let trace = append_eval_trace trace lxp in let eval' lxp ctx = eval lxp ctx trace in @@ -455,13 +455,13 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info) sinfo : (valu (* ---------------- *) | Let(_, decls, inst) -> let nctx = eval_decls decls ctx trace in - eval' inst nctx sinfo + eval' inst nctx (* Function call *) | Call (f, args) -> eval_call (elexp_location f) f trace - (eval f ctx trace sinfo) - (List.map (fun e -> eval e ctx trace sinfo) args) + (eval f ctx trace ) + (List.map (fun e -> eval e ctx trace ) args) (* Case *) | Case (loc, target, pat, dflt) @@ -510,8 +510,8 @@ and eval_call loc unef i f args = -> bindargs e vs (add_rte_variable x v ctx) | ([], _) -> let trace = append_typer_trace i unef in - eval e ctx trace dummy_sinfo - | _ -> eval_call loc unef i (eval e ctx i dummy_sinfo) vs in + eval e ctx trace + | _ -> eval_call loc unef i (eval e ctx i ) vs in bindargs e vs (add_rte_variable x v ctx) | Vbuiltin (name), args @@ -553,12 +553,12 @@ and eval_call loc unef i f args = (* We may call a Vlexp e.g. for "x = Map Int String". * FIXME: The arg will sometimes be a Vlexp but not always, so this is * really just broken! *) - -> Vtype (L.mkCall (e, [(Anormal, mkVar (vdummy, -1) dummy_sinfo)]) dummy_sinfo) + -> Vtype (L.mkCall (e, [(Anormal, mkVar (vdummy, -1) )]) ) | _ -> fatal loc "Trying to call a non-function!\n%s" (trace_value f) and eval_case ctx i loc target pat dflt = (* Eval target *) - let v = eval target ctx i dummy_sinfo in + let v = eval target ctx i in (* extract constructor name and arguments *) let ctor_name, args = match v with @@ -586,17 +586,17 @@ and eval_case ctx i loc target pat dflt = | [], [] -> nctx in let nctx = fold2 ctx pat_args args in - eval exp nctx i dummy_sinfo + eval exp nctx i (* Run default *) with Not_found -> (match dflt with | Some (var, lxp) - -> eval lxp (add_rte_variable var v ctx) i dummy_sinfo + -> eval lxp (add_rte_variable var v ctx) i | _ -> error loc "Match Failure") and build_arg_list args ctx i = (* eval every args *) - let arg_val = List.map (fun (_k, e) -> eval e ctx i dummy_sinfo) args in + let arg_val = List.map (fun (_k, e) -> eval e ctx i ) args in (* Add args inside context *) List.fold_left (fun c v -> add_rte_variable vdummy v c) ctx arg_val @@ -611,7 +611,7 @@ and eval_decls (decls: (vname * elexp) list) add_rte_variable name Vundefined ctx) ctx decls in List.iteri (fun idx (name, lxp) -> - let v = eval lxp nctx i dummy_sinfo in + let v = eval lxp nctx i in let offset = n - idx in ignore (set_rte_variable offset name v nctx)) decls; @@ -798,12 +798,12 @@ let is_bound loc _depth args_val = match args_val with with Senv_Lookup_Fail _ -> false) | _ -> error loc "Elab.isbound takes an Elab_Context and a String as arguments" -let constructor_p name ectx sinfo = +let constructor_p name ectx = try let idx = senv_lookup name ectx in (* 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 ((dummy_location, Some name), idx) sinfo) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx) ) (ectx_to_lctx ectx) with | Cons _ -> true (* It's indeed a constructor! *) | _ -> false with Senv_Lookup_Fail _ -> false @@ -817,7 +817,7 @@ let erasable_p name nth ectx = else false | _ -> false in try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx) dummy_sinfo) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dummy_location, 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 +838,7 @@ let erasable_p2 t name ectx = args) | _ -> false in try let idx = senv_lookup t ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some t), idx) dummy_sinfo) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dummy_location, 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 +856,7 @@ let nth_ctor_arg name nth ectx = | exception (Failure _) -> "_" ) | _ -> "_" in try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx) dummy_sinfo) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dummy_location, 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 +877,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 ((dummy_location, Some name), idx) dummy_sinfo) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dummy_location, 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 @@ -887,7 +887,7 @@ let ctor_arg_pos name arg ectx = with Senv_Lookup_Fail _ -> (-1) let is_constructor loc _depth args_val = match args_val with - | [Vstring name; Velabctx ectx] -> o2v_bool (constructor_p name ectx dummy_sinfo) + | [Vstring name; Velabctx ectx] -> o2v_bool (constructor_p name ectx ) | _ -> error loc "Elab.isconstructor takes a String and an Elab_Context as arguments" let is_nth_erasable loc _depth args_val = match args_val with @@ -1151,7 +1151,7 @@ let from_lctx (lctx: lexp_context): runtime_env = ref (match def with | LetDef (_, e) -> if closed_p rctx (OL.fv e) then - eval (OL.erase_type lctx e) rctx dummy_sinfo + eval (OL.erase_type lctx e) rctx else Vundefined | _ -> Vundefined)) rctx @@ -1173,7 +1173,7 @@ let from_lctx (lctx: lexp_context): runtime_env = * are present! *) let lctx' = DB.lctx_extend_rec lctx defs in if alldefs && closed_p rctx (OL.fv_hoist (List.length defs) fvs) then - List.iter (fun (e, rc) -> rc := eval (OL.erase_type lctx' e) nrctx dummy_sinfo) evs + List.iter (fun (e, rc) -> rc := eval (OL.erase_type lctx' e) nrctx ) evs else () in nrctx and from_lctx lctx = @@ -1201,7 +1201,7 @@ class ast_interpreter lctx = object method eval_expr lexp = let elexp = Opslexp.erase_type lctx lexp in - debug_eval elexp rctx dummy_sinfo + debug_eval elexp rctx method print_rte_ctx = Env.print_rte_ctx rctx ===================================== src/heap.ml ===================================== @@ -39,8 +39,8 @@ let error ~(loc : location) ?print_action fmt = let dloc = Util.dummy_location let type0 = Debruijn.type0 -let type_datacons_label = mkBuiltin ((dloc, "DataconsLabel"), type0) dummy_sinfo -let type_heap = mkBuiltin ((dloc, "Heap"), type_arrow_0) dummy_sinfo +let type_datacons_label = mkBuiltin ((dloc, "DataconsLabel"), type0) +let type_heap = mkBuiltin ((dloc, "Heap"), type_arrow_0) let next_free_address : addr ref = ref 1 ===================================== src/inverse_subst.ml ===================================== @@ -65,7 +65,7 @@ let transfo (s: subst) : substIR option = | _ -> assert false in let shiftVar (var: lexp) (offset: int): int = - indexOf (mkSusp var (S.shift offset) dummy_sinfo) (* Helper : shift the index of a var *) + indexOf (mkSusp var (S.shift offset) ) (* Helper : shift the index of a var *) in match s with | S.Cons (e, s, o) when is_var e @@ -94,7 +94,7 @@ let sizeOf (s: (int * int) list): int = List.length s let counter = ref 0 let mkVar (idx: int) : lexp = counter := !counter + 1; - mkVar ((U.dummy_location, None), idx) dummy_sinfo + mkVar ((U.dummy_location, None), idx) (** Fill the gap between e_i in the list of couple (e_i, i) by adding dummy variables. @@ -242,7 +242,7 @@ let rec compose_inv_subst (s' : subst) (s : subst) = match s' with | S.Cons (e, s', o) -> let s = shift_inv_subst o s in (* FIXME: Why don't we ever return a Shift? *) - S.cons (apply_inv_subst e s dummy_sinfo) (compose_inv_subst s' s) + S.cons (apply_inv_subst e s ) (compose_inv_subst s' s) | S.Identity o -> (match inverse (shift_inv_subst o s) with | Some s -> s (* FIXME: could also be Ambiguous, depending on `s`. *) @@ -252,66 +252,66 @@ let rec compose_inv_subst (s' : subst) (s : subst) = match s' with * The function presumes that `invertible s` was true. * This can be used like mkSusp/push_susp, but it's not lazy. * This is because it can signal errors Not_invertible or Ambiguous. *) -and apply_inv_subst (e : lexp) (s : subst) sinfo : lexp = +and apply_inv_subst (e : lexp) (s : subst) : lexp = match lexp_lexp' e with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (apply_inv_subst e s dummy_sinfo)) sinfo + | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (apply_inv_subst e s )) | SortLevel (SLlub (e1, e2)) (* FIXME: use mkSLlub? *) - -> mkSortLevel (mkSLlub' (apply_inv_subst e1 s dummy_sinfo, apply_inv_subst e2 s dummy_sinfo)) sinfo - | Sort (l, Stype e) -> mkSort (l, Stype (apply_inv_subst e s dummy_sinfo)) sinfo + -> mkSortLevel (mkSLlub' (apply_inv_subst e1 s , apply_inv_subst e2 s )) + | Sort (l, Stype e) -> mkSort (l, Stype (apply_inv_subst e s )) | Sort (_l, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e - | Var (name, i) -> Lexp.mkVar (name, lookup_inv_subst i s) sinfo - | Susp (e, s') -> apply_inv_subst (push_susp e s' dummy_sinfo) s sinfo + | Var (name, i) -> Lexp.mkVar (name, lookup_inv_subst i s) + | Susp (e, s') -> apply_inv_subst (push_susp e s' ) s | Let (l, defs, e) - -> let s' = L.fold_left (fun s (v, _, _) -> ssink dummy_sinfo v s) s defs in + -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty) - -> (ssink dummy_sinfo v s, - (v, apply_inv_subst def s' dummy_sinfo, apply_inv_subst ty s dummy_sinfo) + -> (ssink v s, + (v, apply_inv_subst def s' , apply_inv_subst ty s ) :: ndefs)) (s, []) defs in - mkLet (l, ndefs, apply_inv_subst e s' dummy_sinfo) sinfo + mkLet (l, ndefs, apply_inv_subst e s' ) | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, apply_inv_subst t1 s dummy_sinfo, l, - apply_inv_subst t2 (ssink dummy_sinfo v s) dummy_sinfo) sinfo + -> mkArrow (ak, v, apply_inv_subst t1 s , l, + apply_inv_subst t2 (ssink v s) ) | Lambda (ak, v, t, e) - -> mkLambda (ak, v, apply_inv_subst t s dummy_sinfo, apply_inv_subst e (ssink dummy_sinfo v s) dummy_sinfo) sinfo + -> mkLambda (ak, v, apply_inv_subst t s , apply_inv_subst e (ssink v s) ) | Call (f, args) - -> mkCall (apply_inv_subst f s dummy_sinfo, - L.map (fun (ak, arg) -> (ak, apply_inv_subst arg s dummy_sinfo)) args) sinfo + -> mkCall (apply_inv_subst f s , + L.map (fun (ak, arg) -> (ak, apply_inv_subst arg s )) args) | Inductive (l, label, args, cases) -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink dummy_sinfo v s, (ak, v, apply_inv_subst t s dummy_sinfo) :: nargs)) + -> (ssink v s, (ak, v, apply_inv_subst t s ) :: nargs)) (s, []) args in let nargs = List.rev nargs in let ncases = SMap.map (fun args -> let (_, ncase) = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink dummy_sinfo v s, - (ak, v, apply_inv_subst t s dummy_sinfo) + -> (ssink v s, + (ak, v, apply_inv_subst t s ) :: nargs)) (s, []) args in L.rev ncase) cases in - mkInductive (l, label, nargs, ncases) sinfo - | Cons (it, name) -> mkCons (apply_inv_subst it s dummy_sinfo, name) sinfo + mkInductive (l, label, nargs, ncases) + | Cons (it, name) -> mkCons (apply_inv_subst it s , name) | Case (l, e, ret, cases, default) - -> mkCase (l, apply_inv_subst e s dummy_sinfo, apply_inv_subst ret s dummy_sinfo, + -> mkCase (l, apply_inv_subst e s , apply_inv_subst ret s , SMap.map (fun (l, cargs, e) -> let s' = L.fold_left - (fun s (_,ov) -> ssink dummy_sinfo ov s) + (fun s (_,ov) -> ssink ov s) s cargs in - let s'' = ssink dummy_sinfo (l, None) s' in - (l, cargs, apply_inv_subst e s'' dummy_sinfo )) + let s'' = ssink (l, None) s' in + (l, cargs, apply_inv_subst e s'' )) cases, match default with | None -> default - | Some (v,e) -> Some (v, apply_inv_subst e (ssink dummy_sinfo (l, None) (ssink dummy_sinfo v s)) dummy_sinfo)) sinfo + | Some (v,e) -> Some (v, apply_inv_subst e (ssink (l, None) (ssink v s)) )) | Metavar (id, s', name) -> match metavar_lookup id with - | MVal e -> apply_inv_subst (push_susp e s' dummy_sinfo) s sinfo - | MVar _ -> mkMetavar (id, compose_inv_subst s' s, name) sinfo + | MVal e -> apply_inv_subst (push_susp e s' ) s + | MVar _ -> mkMetavar (id, compose_inv_subst s' s, name) ===================================== src/lexp.ml ===================================== @@ -36,14 +36,13 @@ module S = Subst type vname = U.vname type vref = U.vref type meta_id = int (* Identifier of a meta variable. *) -type sinfo = sexp list +type sinfo = sexp type label = symbol include Pexp.ArgKind -let dummy_sinfo : sexp list = [] (*************** Elaboration to Lexp *********************) @@ -63,32 +62,32 @@ let dummy_sinfo : sexp list = [] type ltype = lexp and subst = lexp S.subst (* Here we want a pair of `Lexp` and its hash value to avoid re-hashing "sub-Lexp". *) - and lexp = lexp' * int * sinfo + and lexp = lexp' * int and lexp' = | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level - | Sort of U.location * sort + | Sort of sinfo * sort | Builtin of symbol * ltype | Var of vref | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) - | Let of U.location * (vname * lexp * ltype) list * lexp - | Arrow of arg_kind * vname * ltype * U.location * ltype + | Let of sinfo * (vname * lexp * ltype) list * lexp + | Arrow of arg_kind * vname * ltype * sinfo * ltype | Lambda of arg_kind * vname * ltype * lexp | Call of lexp * (arg_kind * lexp) list (* Curried call. *) - | Inductive of U.location * label + | Inductive of sinfo * label * ((arg_kind * vname * ltype) list) (* formal Args *) * ((arg_kind * vname * ltype) list) SMap.t | Cons of lexp * symbol (* = Type info * ctor_name *) - | Case of U.location * lexp + | Case of sinfo * lexp * ltype (* The type of the return value of all branches *) - * (U.location * (arg_kind * vname) list * lexp) SMap.t + * (sinfo * (arg_kind * vname) list * lexp) SMap.t * (vname * lexp) option (* Default. *) (* The `subst` will be applied to the the metavar's value when it * gets instantiated. *) | Metavar of meta_id * subst * vname (* (\* For logical metavars, there's no substitution. *\) - * | Metavar of (U.location * string) * metakind * metavar ref + * | Metavar of (sinfo * string) * metakind * metavar ref * and metavar = * (\* An uninstantiated var, along with a venv (stipulating over which vars * * it should be closed), and its type. @@ -181,8 +180,8 @@ let metavar_lookup (id : meta_id) : metavar_info * biggest bucket length: 205 / 36 * found/new lexp entries: - / 2 *) -let lexp_lexp' (e, _h, _) = e -let lexp_hash (_e, h, _) = h +let lexp_lexp' (e, _h) = e +let lexp_hash (_e, h) = h (* Hash `Lexp` using combine_hash (lxor) with hash of "sub-lexp". *) let lexp'_hash (lp : lexp') = @@ -305,28 +304,28 @@ module WHC = Weak.Make (struct type t = lexp let hc_table : WHC.t = WHC.create 1000 -let hc (l : lexp') (sinfo: sexp list) : lexp = - WHC.merge hc_table (l, lexp'_hash l, sinfo) - -let mkImm s sinfo = hc (Imm s) sinfo -let mkSortLevel l sinfo = hc (SortLevel l) sinfo -let mkSort (l, s) sinfo = hc (Sort (l, s)) sinfo -let mkBuiltin (v, t) sinfo = hc (Builtin (v, t)) sinfo -let mkVar v sinfo = hc (Var v) sinfo -let mkLet (l, ds, e) sinfo = hc (Let (l, ds, e)) sinfo -let mkArrow (k, v, t1, l, t2) sinfo = hc (Arrow (k, v, t1, l, t2)) sinfo -let mkLambda (k, v, t, e) sinfo = hc (Lambda (k, v, t, e)) sinfo -let mkInductive (l, n, a, cs) sinfo = hc (Inductive (l, n, a, cs)) sinfo -let mkCons (t, n) sinfo = hc (Cons (t, n)) sinfo -let mkCase (l, e, rt, bs, d) sinfo = hc (Case (l, e, rt, bs, d)) sinfo -let mkMetavar (n, s, v) sinfo = hc (Metavar (n, s, v)) sinfo -let mkCall (f, es) sinfo = +let hc (l : lexp') : lexp = + WHC.merge hc_table (l, lexp'_hash l) + +let mkImm s = hc (Imm s) +let mkSortLevel l = hc (SortLevel l) +let mkSort (l, s) = hc (Sort (l, s)) +let mkBuiltin (v, t) = hc (Builtin (v, t)) +let mkVar v = hc (Var v) +let mkLet (l, ds, e) = hc (Let (l, ds, e)) +let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2)) +let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) +let mkInductive (l, n, a, cs) = hc (Inductive (l, n, a, cs)) +let mkCons (t, n) = hc (Cons (t, n)) +let mkCase (l, e, rt, bs, d) = hc (Case (l, e, rt, bs, d)) +let mkMetavar (n, s, v) = hc (Metavar (n, s, v)) +let mkCall (f, es) = match lexp_lexp' f, es with - | Call (f', es'), _ -> hc (Call (f', es' @ es)) sinfo + | Call (f', es'), _ -> hc (Call (f', es' @ es)) | _, [] -> f - | _ -> hc (Call (f, es)) sinfo + | _ -> hc (Call (f, es)) -let impossible = mkImm Sexp.dummy_epsilon [] +let impossible = mkImm Sexp.dummy_epsilon let lexp_head e = match lexp_lexp' e with @@ -443,7 +442,7 @@ let hcs_table : ((lexp * subst), lexp) Hashtbl.t = Hashtbl.create 1000 * ... *) -let rec mkSusp e s sinfo = +let rec mkSusp e s = if S.identity_p s then e else (* We apply the substitution eagerly to some terms. * There's no deep technical reason for that: @@ -452,21 +451,21 @@ let rec mkSusp e s sinfo = | Imm _ -> e | Builtin _ -> e | Susp (e, s') -> mkSusp_memo e (scompose s' s ) - | Var (l, v) -> slookup s l v sinfo - | Metavar (vn, s', vd) -> mkMetavar (vn, scompose s' s , vd) sinfo - | _ -> hc (Susp (e, s)) sinfo + | Var (l, v) -> slookup s l v + | Metavar (vn, s', vd) -> mkMetavar (vn, scompose s' s , vd) + | _ -> hc (Susp (e, s)) and mkSusp_memo e s = if Hashtbl.mem hcs_table (e, s) then Hashtbl.find hcs_table (e, s) - else let res = mkSusp e s [] in + else let res = mkSusp e s in Hashtbl.add hcs_table (e, s) res; res and scompose s1 s2 = S.compose mkSusp_memo s1 s2 -and slookup s l v sinfo = S.lookup (fun l i -> mkVar (l, i) sinfo) - (fun e o -> mkSusp e (S.shift o) sinfo) +and slookup s l v = S.lookup (fun l i -> mkVar (l, i) ) + (fun e o -> mkSusp e (S.shift o) ) s l v -let ssink sinfo = S.sink (fun l i -> mkVar (l, i) sinfo) +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. @@ -475,7 +474,7 @@ let ssink sinfo = S.sink (fun l i -> mkVar (l, i) sinfo) * one stored in the lctx! * Using DeBruijn *should* make α-renaming unnecessary * so this is a real PITA! :-( *) -let srename name le = mkSusp le (S.cons (mkVar (name, 0) dummy_sinfo) (S.shift 1)) dummy_sinfo +let srename name le = mkSusp le (S.cons (mkVar (name, 0) ) (S.shift 1)) (* Shift by a negative amount! *) let rec sunshift n = @@ -515,20 +514,20 @@ let rec lexp_location e = | Sort (l,_) -> l | SortLevel (SLsucc e) -> lexp_location e | SortLevel (SLlub (e, _)) -> lexp_location e - | SortLevel SLz -> U.dummy_location - | Imm s -> sexp_location s - | Var ((l,_),_) -> l - | Builtin ((l, _), _) -> l + | SortLevel SLz -> dummy_sinfo + | Imm s -> s + | Var ((l,_),_) -> dummy_sinfo + | Builtin ((l, _), _) -> dummy_sinfo | Let (l,_,_) -> l | Arrow (_,_,_,l,_) -> l - | Lambda (_,(l,_),_,_) -> l + | Lambda (_,(l,_),_,_) -> dummy_sinfo | Call (f,_) -> lexp_location f | Inductive (l,_,_,_) -> l - | Cons (_,(l,_)) -> l + | Cons (_,(l,_)) -> dummy_sinfo | Case (l,_,_,_,_) -> l | Susp (e, _) -> lexp_location e (* | Susp (_, e) -> lexp_location e *) - | Metavar (_,_,(l,_)) -> l + | Metavar (_,_,(l,_)) -> dummy_sinfo (********* Normalizing a term *********) @@ -537,132 +536,132 @@ let vdummy = (U.dummy_location, None) let maybename n = match n with None -> "<anon>" | Some v -> v let sname (l,n) = (l, maybename n) -let rec push_susp e s sinfo = (* Push a suspension one level down. *) +let rec push_susp e s = (* Push a suspension one level down. *) match lexp_lexp' e with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e'') -> mkSortLevel (mkSLsucc (mkSusp e'' s sinfo)) sinfo + | SortLevel (SLsucc e'') -> mkSortLevel (mkSLsucc (mkSusp e'' s )) | SortLevel (SLlub (e1, e2)) - -> mkSortLevel (mkSLlub' (mkSusp e1 s sinfo, mkSusp e2 s sinfo)) sinfo - | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s sinfo)) sinfo + -> mkSortLevel (mkSLlub' (mkSusp e1 s , mkSusp e2 s )) + | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s )) | Sort (_, _) -> e | Builtin _ -> e | Let (l, defs, e) - -> let s' = L.fold_left (fun s (v, _, _) -> ssink sinfo v s) s defs in + -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in let rec loop s defs = match defs with | [] -> [] | (v, def, ty) :: defs - -> (v, mkSusp def s' sinfo, mkSusp ty s sinfo) :: loop (ssink sinfo v s) defs in - mkLet (l, loop s defs, mkSusp e s' sinfo) sinfo + -> (v, mkSusp def s' , mkSusp ty s ) :: loop (ssink v s) defs in + mkLet (l, loop s defs, mkSusp e s' ) | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, mkSusp t1 s sinfo, l, mkSusp t2 (ssink sinfo v s) sinfo) sinfo - | Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s sinfo, mkSusp e (ssink sinfo v s) sinfo) sinfo - | Call (f, args) -> mkCall (mkSusp f s sinfo, - L.map (fun (ak, arg) -> (ak, mkSusp arg s sinfo)) args) sinfo + -> mkArrow (ak, v, mkSusp t1 s , l, mkSusp t2 (ssink v s) ) + | Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s , mkSusp e (ssink v s) ) + | Call (f, args) -> mkCall (mkSusp f s , + L.map (fun (ak, arg) -> (ak, mkSusp arg s )) args) | Inductive (l, label, args, cases) -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink sinfo v s, (ak, v, mkSusp t s sinfo) :: nargs)) + -> (ssink v s, (ak, v, mkSusp t s ) :: nargs)) (s, []) args in let nargs = List.rev nargs in let ncases = SMap.map (fun args -> let (_, ncase) = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink sinfo v s, - (ak, v, mkSusp t s sinfo) + -> (ssink v s, + (ak, v, mkSusp t s ) :: nargs)) (s, []) args in L.rev ncase) cases in - mkInductive (l, label, nargs, ncases) sinfo - | Cons (it, name) -> mkCons (mkSusp it s sinfo, name) sinfo + mkInductive (l, label, nargs, ncases) + | Cons (it, name) -> mkCons (mkSusp it s , name) | Case (l, e, ret, cases, default) - -> mkCase (l, mkSusp e s sinfo, mkSusp ret s sinfo, - SMap.map (fun (l, cargs, e) + -> mkCase (l, mkSusp e s , mkSusp ret s , + SMap.map (fun ((l: sinfo), cargs, e) -> let s' = L.fold_left - (fun s (_,ov) -> ssink sinfo ov s) + (fun s (_,ov) -> ssink ov s) s cargs in - (l, cargs, mkSusp e (ssink sinfo (l, None) s') sinfo)) + (l, cargs, mkSusp e (ssink (l, None) s') )) cases, match default with | None -> default - | Some (v,e) -> Some (v, mkSusp e (ssink sinfo (l, None) (ssink sinfo v s)) sinfo)) sinfo + | Some (v,e) -> Some (v, mkSusp e (ssink (l, None) (ssink v s)) )) (* Susp should never appear around Var/Susp/Metavar because mkSusp * pushes the subst into them eagerly. IOW if there's a Susp(Var..) * or Susp(Metavar..) it's because some chunk of code should use mkSusp * rather than Susp. * But we still have to handle them here, since push_susp is called * in many other cases than just when we bump into a Susp. *) - | Susp (e,s') -> push_susp e (scompose s' s) sinfo - | (Var _ | Metavar _) -> nosusp (mkSusp e s sinfo) + | Susp (e,s') -> push_susp e (scompose s' s) + | (Var _ | Metavar _) -> nosusp (mkSusp e s ) and nosusp (e: lexp ) = (* Return `e` with no outermost `Susp`. *) match lexp_lexp' e with - | Susp(e, s) -> push_susp e s dummy_sinfo + | Susp(e, s) -> push_susp e s | _ -> e (* Get rid of `Susp`ensions and instantiated `Metavar`s. *) -let clean e sinfo = +let clean e = let rec clean s e = match lexp_lexp' e with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (clean s e)) sinfo + | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (clean s e)) | SortLevel (SLlub (e1, e2)) (* FIXME: The new SLlub could have `succ` on both sides! *) - -> mkSortLevel (mkSLlub' (clean s e1, clean s e2)) sinfo - | Sort (l, Stype e) -> mkSort (l, Stype (clean s e)) sinfo + -> mkSortLevel (mkSLlub' (clean s e1, clean s e2)) + | Sort (l, Stype e) -> mkSort (l, Stype (clean s e)) | Sort (_, _) -> e | Builtin _ -> e | Let (l, defs, e) - -> let s' = L.fold_left (fun s (v, _, _) -> ssink sinfo v s) s defs in + -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty) - -> (ssink sinfo v s, + -> (ssink v s, (v, clean s' def, clean s ty) :: ndefs)) (s, []) defs in - mkLet (l, ndefs, clean s' e) sinfo + mkLet (l, ndefs, clean s' e) | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, clean s t1, l, clean (ssink sinfo v s) t2) sinfo - | Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink sinfo v s) e) sinfo + -> mkArrow (ak, v, clean s t1, l, clean (ssink v s) t2) + | Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink v s) e) | Call (f, args) -> mkCall (clean s f, - L.map (fun (ak, arg) -> (ak, clean s arg)) args) sinfo + L.map (fun (ak, arg) -> (ak, clean s arg)) args) | Inductive (l, label, args, cases) -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink sinfo v s, (ak, v, clean s t) :: nargs)) + -> (ssink v s, (ak, v, clean s t) :: nargs)) (s, []) args in let nargs = List.rev nargs in let ncases = SMap.map (fun args -> let (_, ncase) = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink sinfo v s, + -> (ssink v s, (ak, v, clean s t) :: nargs)) (s, []) args in L.rev ncase) cases in - mkInductive (l, label, nargs, ncases) sinfo - | Cons (it, name) -> mkCons (clean s it, name) sinfo + mkInductive (l, label, nargs, ncases) + | Cons (it, name) -> mkCons (clean s it, name) | Case (l, e, ret, cases, default) -> mkCase (l, clean s e, clean s ret, SMap.map (fun (l, cargs, e) -> let s' = L.fold_left - (fun s (_,ov) -> ssink sinfo ov s) + (fun s (_,ov) -> ssink ov s) s cargs in - let s'' = ssink sinfo (l, None) s' in + let s'' = ssink (l, None) s' in (l, cargs, clean s'' e)) cases, match default with | None -> default - | Some (v,e) -> Some (v, clean (ssink sinfo (l, None) (ssink sinfo v s)) e)) sinfo + | Some (v,e) -> Some (v, clean (ssink (l, None) (ssink v s)) e)) | Susp (e, s') -> clean (scompose s' s) e | Var _ -> if S.identity_p s then e - else clean S.identity (mkSusp e s sinfo) + else clean S.identity (mkSusp e s ) | Metavar (idx, s', name) -> let s = scompose s' s in match metavar_lookup idx with | MVal e -> clean s e - | _ -> mkMetavar (idx, s, name) sinfo + | _ -> mkMetavar (idx, s, name) in clean S.identity e let sdatacons = Symbol (U.dummy_location, "##datacons") @@ -913,14 +912,14 @@ and lexp_string e = lexp_cstring (!debug_ppctx) e (* Context Print *) and lexp_cprint ctx e = print_string (lexp_cstring ctx e ) -and lexp_cstring ctx e = lexp_str ctx e dummy_sinfo +and lexp_cstring ctx e = lexp_str ctx e (* Implementation *) -and lexp_str ctx (exp : lexp) sinfo : string = +and lexp_str ctx (exp : lexp) : string = let inter_ctx = add_indent ctx 1 in - let lexp_str' sinfo = lexp_str ctx sinfo in - let lexp_stri idt e sinfo = lexp_str (add_indent ctx idt) e sinfo in + let lexp_str' = lexp_str ctx in + let lexp_stri idt e = lexp_str (add_indent ctx idt) e in let pretty = pp_pretty ctx in let color = pp_color ctx in @@ -974,14 +973,14 @@ and lexp_str ctx (exp : lexp) sinfo : string = | Float (_, s) -> tval (string_of_float s) | e -> sexp_string e) - | Susp (e, s) -> lexp_str ctx (push_susp e s sinfo) sinfo + | Susp (e, s) -> lexp_str ctx (push_susp e s ) | Var ((_loc, name), idx) -> maybename name ^ (index idx) ; | Metavar (idx, subst, (_loc, name)) (* print metavar result if any *) -> (match metavar_lookup idx with - | MVal e -> lexp_str ctx (push_susp e subst sinfo) sinfo + | MVal e -> lexp_str ctx (push_susp e subst ) | _ -> "?" ^ maybename name ^ (subst_string subst ) ^ (index idx)) | Let (_, decls, body) -> @@ -1001,35 +1000,35 @@ and lexp_str ctx (exp : lexp) sinfo : string = else decls in (keyword "let ") ^ decls ^ (keyword " in ") ^ newline ^ - (make_indent idt_lvl) ^ (lexp_stri idt_lvl body sinfo) + (make_indent idt_lvl) ^ (lexp_stri idt_lvl body ) | Arrow(k, (_, Some name), tp, _loc, expr) -> - "(" ^ name ^ " : " ^ (lexp_str' tp sinfo) ^ ") " ^ - (kind_str k) ^ " " ^ (lexp_str' expr sinfo) + "(" ^ name ^ " : " ^ (lexp_str' tp ) ^ ") " ^ + (kind_str k) ^ " " ^ (lexp_str' expr ) | Arrow(k, (_, None), tp, _loc, expr) -> - "(" ^ (lexp_str' tp sinfo) ^ " " - ^ (kind_str k) ^ " " ^ (lexp_str' expr sinfo) ^ ")" + "(" ^ (lexp_str' tp ) ^ " " + ^ (kind_str k) ^ " " ^ (lexp_str' expr ) ^ ")" | Lambda(k, (_loc, name), ltype, lbody) -> - let arg = "(" ^ maybename name ^ " : " ^ (lexp_str' ltype sinfo) ^ ")" in + let arg = "(" ^ maybename name ^ " : " ^ (lexp_str' ltype ) ^ ")" in (keyword "lambda ") ^ arg ^ " " ^ (kind_str k) ^ newline ^ - (make_indent 1) ^ (lexp_stri 1 lbody sinfo) + (make_indent 1) ^ (lexp_stri 1 lbody ) | Cons(t, (_, ctor_name)) -> - (keyword "datacons ") ^ (lexp_str' t sinfo) ^ " " ^ ctor_name + (keyword "datacons ") ^ (lexp_str' t ) ^ " " ^ ctor_name | Call(fname, args) -> let name, idx = get_name fname in let binop_str op (_, lhs) (_, rhs) = - "(" ^ (lexp_str' lhs sinfo) ^ op ^ (index idx) ^ " " ^ (lexp_str' rhs sinfo) ^ ")" in + "(" ^ (lexp_str' lhs ) ^ op ^ (index idx) ^ " " ^ (lexp_str' rhs ) ^ ")" in let print_arg str (arg_type, lxp) = match arg_type with - | Aerasable when pp_erasable ctx -> str ^ " " ^ (lexp_str' lxp sinfo) - | Aimplicit when pp_implicit ctx -> str ^ " " ^ (lexp_str' lxp sinfo) - | Anormal -> str ^ " " ^ (lexp_str' lxp sinfo) + | Aerasable when pp_erasable ctx -> str ^ " " ^ (lexp_str' lxp ) + | Aimplicit when pp_implicit ctx -> str ^ " " ^ (lexp_str' lxp ) + | Anormal -> str ^ " " ^ (lexp_str' lxp ) | _ -> str in ( match args with @@ -1037,7 +1036,7 @@ and lexp_str ctx (exp : lexp) sinfo : string = binop_str (" " ^ (get_binary_op_name name)) lhs rhs | _ -> let args = List.fold_left print_arg "" args in - "(" ^ (lexp_str' fname sinfo) ^ args ^ ")") + "(" ^ (lexp_str' fname ) ^ args ^ ")") | Inductive (_, (_, name), [], ctors) -> (keyword "typecons") ^ " (" ^ name ^") " ^ newline ^ @@ -1048,14 +1047,14 @@ and lexp_str ctx (exp : lexp) sinfo : string = = List.fold_left (fun str (arg_kind, (_, name), ltype) -> str ^ " (" ^ maybename name ^ " " ^ (kindp_str arg_kind) ^ " " - ^ (lexp_str' ltype sinfo) ^ ")") + ^ (lexp_str' ltype ) ^ ")") "" args in (keyword "typecons") ^ " (" ^ name ^ args_str ^") " ^ (lexp_str_ctor ctx ctors ) | Case (_, target, _ret, map, dflt) ->( - let str = (keyword "case ") ^ (lexp_str' target sinfo) in + let str = (keyword "case ") ^ (lexp_str' target ) in let arg_str arg = List.fold_left (fun str v -> match v with @@ -1065,7 +1064,7 @@ and lexp_str ctx (exp : lexp) sinfo : string = let str = SMap.fold (fun k (_, arg, exp) str -> str ^ nl ^ (make_indent 1) ^ - "| " ^ (fun_call k) ^ (arg_str arg) ^ " => " ^ (lexp_stri 1 exp sinfo)) + "| " ^ (fun_call k) ^ (arg_str arg) ^ " => " ^ (lexp_stri 1 exp )) map str in match dflt with @@ -1074,7 +1073,7 @@ and lexp_str ctx (exp : lexp) sinfo : string = str ^ nl ^ (make_indent 1) ^ "| " ^ (match v with (_, None) -> "_" | (_, Some name) -> name) - ^ " => " ^ (lexp_stri 1 df sinfo)) + ^ " => " ^ (lexp_stri 1 df )) | Builtin ((_, name), _) -> "##" ^ name @@ -1103,7 +1102,7 @@ and lexp_str_ctor ctx ctors = SMap.fold (fun key value str -> let str = str ^ newline ^ (make_indent 1) ^ "(" ^ key in let str = List.fold_left (fun str (_k, _, arg) - -> str ^ " " ^ (lexp_str ctx arg dummy_sinfo)) + -> str ^ " " ^ (lexp_str ctx arg )) str value in str ^ ")") ctors "" @@ -1114,13 +1113,13 @@ and lexp_str_decls ctx decls = let sepdecl = (if pp_decl ctx then "\n" else "") in let type_str name lxp = (if pp_type ctx then ( - name ^ " : " ^ (lexp_str' lxp dummy_sinfo) ^ ";") else "") in + name ^ " : " ^ (lexp_str' lxp ) ^ ";") else "") in let ret = List.fold_left (fun str ((_, name), lxp, ltp) -> let name = maybename name in let str = if pp_type ctx then (type_str name ltp)::str else str in - (name ^ " = " ^ (lexp_str' lxp dummy_sinfo) ^ ";" ^ sepdecl)::str) + (name ^ " = " ^ (lexp_str' lxp ) ^ ";" ^ sepdecl)::str) [] decls in List.rev ret @@ -1139,8 +1138,8 @@ let rec eq e1 e2 = | (Sort (_, Stype e1), Sort (_, Stype e2)) -> eq e1 e2 | (Builtin ((_, name1), _), Builtin ((_, name2), _)) -> name1 = name2 | (Var (_, i1), Var (_, i2)) -> i1 = i2 - | (Susp (e1, s1), _) -> eq (push_susp e1 s1 dummy_sinfo) e2 - | (_, Susp (e2, s2)) -> eq e1 (push_susp e2 s2 dummy_sinfo) + | (Susp (e1, s1), _) -> eq (push_susp e1 s1 ) e2 + | (_, Susp (e2, s2)) -> eq e1 (push_susp e2 s2 ) | (Let (_, defs1, e1), Let (_, defs2, e2)) -> eq e1 e2 && List.for_all2 (fun (_, e1, t1) (_, e2, t2) -> eq t1 t2 && eq e1 e2 ) defs1 defs2 @@ -1167,16 +1166,16 @@ let rec eq e1 e2 = | (Metavar (i1, s1, _), Metavar (i2, s2, _)) -> if i1 == i2 then subst_eq s1 s2 else (match (metavar_lookup i1, metavar_lookup i2) with - | (MVal l, _) -> eq (push_susp l s1 dummy_sinfo) e2 - | (_, MVal l) -> eq e1 (push_susp l s2 dummy_sinfo) + | (MVal l, _) -> eq (push_susp l s1 ) e2 + | (_, MVal l) -> eq e1 (push_susp l s2 ) | _ -> false) | (Metavar (i1, s1, _), _) -> (match metavar_lookup i1 with - | MVal l -> eq (push_susp l s1 dummy_sinfo) e2 + | MVal l -> eq (push_susp l s1 ) e2 | _ -> false) | (_, Metavar (i2, s2, _)) -> (match metavar_lookup i2 with - | MVal l -> eq e1 (push_susp l s2 dummy_sinfo) + | MVal l -> eq e1 (push_susp l s2 ) | _ -> false) | _ -> false with @@ -1191,10 +1190,10 @@ and subst_eq s1 s2 = eq e1 e2 && subst_eq s1 s2 else if o1 > o2 then let o = o1 - o2 in - eq (mkSusp e1 (S.shift o) dummy_sinfo) e2 + eq (mkSusp e1 (S.shift o) ) e2 && subst_eq (S.mkShift s1 o) s2 else let o = o2 - o1 in - eq e1 (mkSusp e2 (S.shift o) dummy_sinfo) + eq e1 (mkSusp e2 (S.shift o) ) && subst_eq s1 (S.mkShift s2 o) | _ -> false ===================================== src/opslexp.ml ===================================== @@ -108,7 +108,7 @@ let lookup_value = DB.lctx_lookup_value let rec lexp_defs_subst l s defs = match defs with | [] -> s | (_, lexp, _) :: defs' - -> lexp_defs_subst l (S.cons (mkLet (l, defs, lexp) dummy_sinfo) s) defs' + -> lexp_defs_subst l (S.cons (mkLet (l, defs, lexp) ) s) defs' (** Convert a lexp_context into a substitution. *) @@ -124,7 +124,7 @@ let rec lctx_to_subst lctx = * Another option would be to map them to `L.impossible`, * hence making the target domain be empty (i.e. making the substitution * generate closed results). *) - L.ssink dummy_sinfo v s + L.ssink v s | DB.CVfix (defs, lctx) -> let s1 = lctx_to_subst lctx in let s2 = lexp_defs_subst DB.dloc S.identity @@ -142,7 +142,7 @@ let lexp_close lctx e = * - It turns the lctx (of O(log N) access time) into a subst * (of O(N) access time) * Oh well! *) - mkSusp e (lctx_to_subst lctx) dummy_sinfo + mkSusp e (lctx_to_subst lctx) (** Reduce to weak head normal form. @@ -167,34 +167,34 @@ let lexp_close lctx e = the inductive type of the target (and it's typelevel). A better solution would be to add these values as annotations in the lexp datatype. *) -let rec lexp_whnf_aux e (ctx : DB.lexp_context) sinfo : lexp = - let rec lexp_whnf_aux e (ctx : DB.lexp_context) sinfo: lexp = +let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = + let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = match lexp_lexp' e with | Var v -> (match lookup_value ctx v with | None -> e (* We can do this blindly even for recursive definitions! * IOW the risk of inf-looping should only show up when doing * things like full normalization (e.g. lexp_conv_p). *) - | Some e' -> lexp_whnf_aux e' ctx sinfo) - | Susp (e, s) -> lexp_whnf_aux (push_susp e s dummy_sinfo) ctx sinfo - | Call (e, []) -> lexp_whnf_aux e ctx sinfo + | Some e' -> lexp_whnf_aux e' ctx ) + | Susp (e, s) -> lexp_whnf_aux (push_susp e s ) ctx + | Call (e, []) -> lexp_whnf_aux e ctx | Call (f, (((_, arg)::args) as xs)) -> - (match lexp_lexp' (lexp_whnf_aux f ctx sinfo) with + (match lexp_lexp' (lexp_whnf_aux f ctx ) with | Lambda (_, _, _, body) -> (* Here we apply whnf to the arg eagerly to kind of stay closer * to the idea of call-by-value, although in this context * we can't really make sure we always reduce the arg to a value. *) - lexp_whnf_aux (mkCall (push_susp body (S.substitute (lexp_whnf_aux arg ctx dummy_sinfo)) dummy_sinfo, - args) dummy_sinfo) - ctx sinfo - | Call (f', xs1) -> mkCall (f', List.append xs1 xs) sinfo + lexp_whnf_aux (mkCall (push_susp body (S.substitute (lexp_whnf_aux arg ctx )) , + args) ) + ctx + | Call (f', xs1) -> mkCall (f', List.append xs1 xs) | Builtin ((_, name), _) -> (match SMap.find_opt name (!reducible_builtins) with | Some f -> Option.value ~default:e (f ctx args) | None -> e) | _ -> e) (* Keep `e`, assuming it's more readable! *) | Case (l, e, rt, branches, default) -> - let e' = lexp_whnf_aux e ctx sinfo in + let e' = lexp_whnf_aux e ctx in let get_refl e = let etype = get_type ctx e in (* FIXME we should not need get_type here *) let elevel = match lexp'_whnf (get_type ctx etype) ctx with @@ -203,9 +203,9 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) sinfo : lexp = mkCall (DB.eq_refl, [L.Aerasable, elevel; L.Aerasable, etype; - L.Aerasable, e]) dummy_sinfo in + L.Aerasable, e]) in let reduce it name aargs = - let targs = match lexp_lexp' (lexp_whnf_aux it ctx dummy_sinfo) with + let targs = match lexp_lexp' (lexp_whnf_aux it ctx ) with | Inductive (_,_,fargs,_) -> fargs | _ -> Log.log_error "Case on a non-inductive type in whnf!"; [] in try @@ -214,7 +214,7 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) sinfo : lexp = = List.fold_left (fun (s, targs) (_, arg) -> match targs with - | [] -> (S.cons (lexp_whnf_aux arg ctx dummy_sinfo) s, []) + | [] -> (S.cons (lexp_whnf_aux arg ctx ) s, []) | _targ::targs -> (* Ignore the type arguments *) (s, targs)) @@ -222,43 +222,43 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) sinfo : lexp = aargs in (* Substitute case Eq variable by the proof (Eq.refl l t e') *) let subst = S.cons (get_refl e') subst in - lexp_whnf_aux (push_susp branch subst dummy_sinfo) ctx sinfo + lexp_whnf_aux (push_susp branch subst ) ctx with | Not_found -> match default with | Some (_v,default) -> let subst = S.cons (get_refl e') (S.substitute e') in - lexp_whnf_aux (push_susp default subst dummy_sinfo) ctx sinfo + lexp_whnf_aux (push_susp default subst ) ctx | _ -> Log.log_error ~section:"WHNF" ~loc:l {|Unhandled constructor "%s" in case expression|} name; - mkCase (l, e, rt, branches, default) dummy_sinfo in + mkCase (l, e, rt, branches, default) in (match lexp_lexp' e' with | Cons (it, (_, name)) -> reduce it name [] | Call (f, aargs) -> - (match lexp_lexp' (lexp_whnf_aux f ctx sinfo) with + (match lexp_lexp' (lexp_whnf_aux f ctx ) with | Cons (it, (_, name)) -> reduce it name aargs - | _ -> mkCase (l, e, rt, branches, default) dummy_sinfo) - | _ -> mkCase (l, e, rt, branches, default) sinfo) + | _ -> mkCase (l, e, rt, branches, default) ) + | _ -> mkCase (l, e, rt, branches, default) ) | Metavar (idx, s, _) -> (match metavar_lookup idx with - | MVal e -> lexp_whnf_aux (push_susp e s dummy_sinfo) ctx sinfo + | MVal e -> lexp_whnf_aux (push_susp e s ) ctx | _ -> e) (* FIXME: I'd really prefer to use "native" recursive substitutions, using * ideally a trick similar to the db_offsets in lexp_context! *) | Let (l, defs, body) - -> lexp_whnf_aux (push_susp body (lexp_defs_subst l S.identity defs) dummy_sinfo) ctx sinfo + -> lexp_whnf_aux (push_susp body (lexp_defs_subst l S.identity defs) ) ctx | _elem -> e - in lexp_whnf_aux e ctx sinfo + in lexp_whnf_aux e ctx and lexp'_whnf e (ctx : DB.lexp_context) : lexp' = - lexp_lexp' (lexp_whnf_aux e ctx dummy_sinfo) + lexp_lexp' (lexp_whnf_aux e ctx ) and lexp_whnf e (ctx : DB.lexp_context) : lexp = - lexp_whnf_aux e ctx dummy_sinfo + lexp_whnf_aux e ctx and eq_cast_whnf ctx args = match args with @@ -289,7 +289,7 @@ and set_add (s : set_plexp) (e1 : lexp) (e2 : lexp) : set_plexp ((e1, e2) :: s) and set_shift_n (s : set_plexp) (n : U.db_offset) = List.map (let s = S.shift n in - fun (e1, e2) -> (Lexp.push_susp e1 s dummy_sinfo, Lexp.push_susp e2 s dummy_sinfo)) + fun (e1, e2) -> (Lexp.push_susp e1 s , Lexp.push_susp e2 s )) s and set_shift s : set_plexp = set_shift_n s 1 @@ -315,9 +315,9 @@ and level_canon e = | Var (_, i) -> add_var_depth i d acc | Metavar (i, s, _) -> (match metavar_lookup i with - | MVal e -> canon (push_susp e s dummy_sinfo) d acc + | MVal e -> canon (push_susp e s ) d acc | _ -> add_var_depth (- i) d acc) - | Susp (e, s) -> canon (push_susp e s dummy_sinfo) d acc + | Susp (e, s) -> canon (push_susp e s ) d acc | _ -> (max_int, m) in canon e 0 (0,IMap.empty) @@ -429,14 +429,14 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = S.identity fargs aargs in (* 3. Compare the branches *) let ctx_extend_with_eq ctx subst hlxp = - let tlxp = mkSusp target subst dummy_sinfo in - let tltp = mkSusp etype subst dummy_sinfo in - let tlvl = mkSusp elvl subst dummy_sinfo in + let tlxp = mkSusp target subst in + let tltp = mkSusp etype subst in + let tlvl = mkSusp elvl subst in let eqty = mkCall (DB.type_eq, [(L.Aerasable, tlvl); (* Typelevel *) (L.Aerasable, tltp); (* Inductive type *) (L.Anormal, hlxp); (* Lexp of the branch head *) - (L.Anormal, tlxp)]) dummy_sinfo in (* Target lexp *) + (L.Anormal, tlxp)]) in (* Target lexp *) DB.lexp_ctx_cons ctx (DB.dloc, None) Variable eqty in (* The map module doesn't have a function to compare two maps with the key (which is needed to get the field types @@ -453,9 +453,9 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = (ak', _vdef', ftype)::fieldtypes -> if ak1 = ak2 && ak2 = ak' then mkctx - (DB.lexp_ctx_cons ctx vdef1 Variable (mkSusp ftype s dummy_sinfo)) - ((ak1, (mkVar (vdef1, i) dummy_sinfo))::args) - (ssink dummy_sinfo vdef1 s) + (DB.lexp_ctx_cons ctx vdef1 Variable (mkSusp ftype s )) + ((ak1, (mkVar (vdef1, i) ))::args) + (ssink vdef1 s) (i - 1) vdefs1 vdefs2 fieldtypes else None @@ -468,9 +468,9 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let subst = S.shift offset in let eaargs = List.map (fun (_, a) -> (P.Aerasable, a)) aargs in - let ctor = mkSusp (mkCall (mkCons (it, (DB.dloc, l1)) dummy_sinfo, - eaargs) dummy_sinfo) subst dummy_sinfo in - let hlxp = mkCall (ctor, args) dummy_sinfo in + let ctor = mkSusp (mkCall (mkCons (it, (DB.dloc, l1)) , + eaargs) ) subst in + let hlxp = mkCall (ctor, args) in let nctx = ctx_extend_with_eq nctx subst hlxp in conv_p' nctx (set_shift_n vs' (offset + 1)) e1 e2 ) (SMap.bindings cases1) (SMap.bindings cases2) @@ -481,7 +481,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | (Some (v1, e1), Some (_v2, e2)) -> let nctx = DB.lctx_extend ctx v1 Variable etype in let subst = S.shift 1 in - let hlxp = mkVar ((DB.dloc, None), 0) dummy_sinfo in + let hlxp = mkVar ((DB.dloc, None), 0) in let nctx = ctx_extend_with_eq nctx subst hlxp in conv_p' nctx (set_shift_n vs' 2) e1 e2 | None, None -> true @@ -505,13 +505,13 @@ and mkSLlub ctx e1 e2 = | (SortLevel SLz, _) -> e2 | (_, SortLevel SLz) -> e1 | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) - -> mkSortLevel (SLsucc (mkSLlub ctx e1 e2)) dummy_sinfo + -> mkSortLevel (SLsucc (mkSLlub ctx e1 e2)) | (_e1', _e2') -> let ce1 = level_canon lwhnf1 in let ce2 = level_canon lwhnf2 in if level_leq ce1 ce2 then e2 else if level_leq ce2 ce1 then e1 - else mkSortLevel (mkSLlub' (e1, e2)) dummy_sinfo (* FIXME: Could be more canonical *) + else mkSortLevel (mkSLlub' (e1, e2)) (* FIXME: Could be more canonical *) and sort_compose ctx1 ctx2 l ak k1 k2 = (* BEWARE! Technically `k2` can refer to `v`, but this should only happen @@ -523,13 +523,13 @@ and sort_compose ctx1 ctx2 l ak k1 k2 = -> (match s1, s2 with | (Stype l1, Stype l2) -> if ak == P.Aerasable && impredicative_erase - then SortResult (mkSusp k2 (S.substitute impossible) dummy_sinfo) - else let l2' = (mkSusp l2 (S.substitute impossible) dummy_sinfo) in + then SortResult (mkSusp k2 (S.substitute impossible) ) + else let l2' = (mkSusp l2 (S.substitute impossible) ) in (* print_string ("Normal: " ^ lexp_string l1 ^ " -> " * ^ lexp_string l2' ^ " ==> " * ^ lexp_string (mkSort (l, Stype (mkSLlub ctx1 l1 l2'))) * ^ "\n"); *) - SortResult (mkSort (l, Stype (mkSLlub ctx1 l1 l2')) dummy_sinfo) + SortResult (mkSort (l, Stype (mkSLlub ctx1 l1 l2')) ) | (StypeLevel, Stype _l2) when ak == P.Aerasable && impredicative_universe_poly (* The safety/soundness of this rule is completely unknown. @@ -540,7 +540,7 @@ and sort_compose ctx1 ctx2 l ak k1 k2 = * ^ lexp_string k2 ^ " ==> " * ^ lexp_string (mkSusp k2 (S.substitute DB.level0)) * ^ "\n"); *) - SortResult (mkSusp k2 (S.substitute DB.level0) dummy_sinfo) + SortResult (mkSusp k2 (S.substitute DB.level0) ) | (StypeLevel, Stype _) | (StypeLevel, StypeOmega) (* This might be safe, but I don't think it adds much power. @@ -548,7 +548,7 @@ and sort_compose ctx1 ctx2 l ak k1 k2 = * arguments, but let's not bother for now: it's easier to add it * later than to remove it later. * | (Stype _, StypeOmega) *) - -> SortResult (mkSort (l, StypeOmega) dummy_sinfo) + -> SortResult (mkSort (l, StypeOmega) ) | _ -> SortInvalid) | (Sort (_, _), _) -> SortK2NotType | (_, _) -> SortK1NotType @@ -583,7 +583,7 @@ and nerased_let defs erased = erased es (* "check ctx e" should return τ when "Δ ⊢ e : τ" *) -and check'' erased ctx e sinfo = +and check'' erased ctx e = let check = check'' in let assert_type ctx e t t' = if conv_p ctx t t' then () @@ -594,7 +594,7 @@ and check'' erased ctx e sinfo = (lexp_string e) (lexp_string t) (lexp_string t') in let check_type erased ctx t = - let s = check erased ctx t sinfo in + let s = check erased ctx t in (match lexp'_whnf s ctx with | Sort _ -> () | _ @@ -610,21 +610,21 @@ and check'' erased ctx e sinfo = DB.type_int ) | SortLevel SLz -> DB.type_level | SortLevel (SLsucc e) - -> let t = check erased ctx e sinfo in + -> let t = check erased ctx e in (* FIXME: Actually, we should probably have a special function to check * that `e` is a level, so as to avoid `case` and other funny things. *) assert_type ctx e t DB.type_level; DB.type_level | SortLevel (SLlub (e1, e2)) - -> let t1 = check erased ctx e1 sinfo in + -> let t1 = check erased ctx e1 in assert_type ctx e1 t1 DB.type_level; - let t2 = check erased ctx e2 sinfo in + let t2 = check erased ctx e2 in assert_type ctx e2 t2 DB.type_level; DB.type_level | Sort (l, Stype e) - -> let t = check erased ctx e sinfo in + -> let t = check erased ctx e in assert_type ctx e t DB.type_level; - mkSort (l, Stype (mkSortLevel (SLsucc e) dummy_sinfo)) dummy_sinfo + mkSort (l, Stype (mkSortLevel (SLsucc e) )) | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) -> ((* error_tc ~loc:(lexp_location e) "Reached unreachable sort!"; @@ -641,7 +641,7 @@ and check'' erased ctx e sinfo = {|Var `%s` can't be used here, because it's erasable|} (maybename name) ; lookup_type ctx v - | Susp (e, s) -> check erased ctx (push_susp e s dummy_sinfo) sinfo + | Susp (e, s) -> check erased ctx (push_susp e s ) | Let (l, defs, e) -> let _ = List.fold_left (fun ctx (v, _e, t) @@ -657,12 +657,12 @@ and check'' erased ctx e sinfo = (check (if DB.set_mem (n - 1) nerased then DB.set_empty else nerased) - nctx e sinfo) - (push_susp t (S.shift n) dummy_sinfo); + nctx e ) + (push_susp t (S.shift n) ); n - 1) (List.length defs) defs in - mkSusp (check nerased nctx e sinfo) - (lexp_defs_subst l S.identity defs) dummy_sinfo + mkSusp (check nerased nctx e ) + (lexp_defs_subst l S.identity defs) | Arrow (ak, v, t1, loc, t2) -> (let k1 = check_type erased ctx t1 in let nctx = DB.lexp_ctx_cons ctx v Variable t1 in @@ -671,31 +671,31 @@ and check'' erased ctx e sinfo = | SortResult k -> k | SortInvalid -> log_tc_error ~loc "Invalid arrow: inner TypelLevel argument"; - mkSort (loc, StypeOmega) sinfo + mkSort (loc, StypeOmega) | SortK1NotType -> log_tc_error ~loc:(lexp_location t1) "Not a proper type"; - mkSort (loc, StypeOmega) sinfo + mkSort (loc, StypeOmega) | SortK2NotType -> log_tc_error ~loc:(lexp_location t2) "Not a proper type"; - mkSort (loc, StypeOmega) sinfo) + mkSort (loc, StypeOmega) ) | Lambda (ak, ((l,_) as v), t, e) -> (let _k = check_type DB.set_empty ctx t in mkArrow (ak, v, t, l, check (dbset_push ak erased) (DB.lctx_extend ctx v Variable t) - e sinfo) dummy_sinfo) + e ) ) | Call (f, args) - -> let ft = check erased ctx f sinfo in + -> 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) - ctx arg sinfo in + ctx arg in match lexp'_whnf ft ctx with | Arrow (ak', _v, t1, _l, t2) -> if ak != ak' then log_tc_error ~loc:(lexp_location arg) "arg kind mismatch"; assert_type ctx arg at t1; - mkSusp t2 (S.substitute arg) dummy_sinfo + mkSusp t2 (S.substitute arg) | _ -> log_tc_error ~loc:(lexp_location arg) "Calling a non functin (type = %s)!" (lexp_string ft); @@ -722,7 +722,7 @@ and check'' erased ctx e sinfo = * cannot refer to the fields! *) (* FIXME: If it does refer, * we get an ugly error! *) - (mkSusp level' (L.sunshift n) sinfo) + (mkSusp level' (L.sunshift n) ) | _tt -> log_tc_error ~loc:(lexp_location t) @@ -737,14 +737,14 @@ and check'' erased ctx e sinfo = (level, ctx, erased, 0) case in level) - cases (mkSortLevel SLz sinfo) in - mkSort (l, Stype level) sinfo + cases (mkSortLevel SLz ) in + mkSort (l, Stype level) | (ak, v, t)::args -> let _k = check_type DB.set_empty ctx t in mkArrow (ak, v, t, lexp_location t, arg_loop (DB.lctx_extend ctx v Variable t) (dbset_push ak erased) - args) dummy_sinfo in + args) in let tct = arg_loop ctx erased args in tct | Case (l, e, ret, branches, default) @@ -753,7 +753,7 @@ and check'' erased ctx e sinfo = match lexp_lexp' e with | Call (f, args) -> (f, args) | _ -> (e,[]) in - let etype = lexp_whnf (check erased ctx e sinfo) ctx in + let etype = lexp_whnf (check erased ctx e ) ctx in (* FIXME save the type in the case lexp instead of recomputing it over and over again *) let ekind = get_type ctx etype in @@ -776,14 +776,14 @@ and check'' erased ctx e sinfo = s in let s = mksubst S.identity fargs aargs in let ctx_extend_with_eq ctx subst hlxp nerased = - let tlxp = mkSusp e subst dummy_sinfo in - let tltp = mkSusp etype subst dummy_sinfo in - let tlvl = mkSusp elvl subst dummy_sinfo in + let tlxp = mkSusp e subst in + let tltp = mkSusp etype subst in + let tlvl = mkSusp elvl subst in let eqty = mkCall (DB.type_eq, [(L.Aerasable, tlvl); (* Typelevel *) (L.Aerasable, tltp); (* Inductive type *) (L.Anormal, hlxp); (* Lexp of the branch head *) - (L.Anormal, tlxp)]) dummy_sinfo in (* Target lexp *) + (L.Anormal, tlxp)]) in (* Target lexp *) (* The eq proof is erasable. *) let nerased = dbset_push L.Aerasable nerased in let nctx = DB.lexp_ctx_cons ctx (l, None) Variable eqty in @@ -798,23 +798,23 @@ and check'' erased ctx e sinfo = * appears in type annotations. *) | (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes -> mkctx (dbset_push ak erased) - (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s sinfo)) - (ssink dummy_sinfo vdef s) - (mkCall (mkSusp hlxp (S.shift 1) sinfo, [(ak, mkVar (vdef, 0) sinfo)]) sinfo) + (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s )) + (ssink vdef s) + (mkCall (mkSusp hlxp (S.shift 1) , [(ak, mkVar (vdef, 0) )]) ) vdefs fieldtypes | _ -> log_tc_error ~loc:l "Wrong number of args to constructor!"; (erased, ctx, hlxp) in let hctor = - mkCall (mkCons (it, (l, name)) sinfo, - List.map (fun (_, a) -> (P.Aerasable, a)) aargs) dummy_sinfo in + mkCall (mkCons (it, (l, name)) , + List.map (fun (_, a) -> (P.Aerasable, a)) aargs) in let (nerased, nctx, hlxp) = mkctx erased ctx s hctor vdefs fieldtypes in let subst = S.shift (List.length vdefs) in let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp nerased in assert_type nctx branch - (check nerased nctx branch sinfo) - (mkSusp ret (S.shift ((List.length fieldtypes) + 1)) sinfo)) + (check nerased nctx branch ) + (mkSusp ret (S.shift ((List.length fieldtypes) + 1)) )) branches; let diff = SMap.cardinal constructors - SMap.cardinal branches in (match default with @@ -824,11 +824,11 @@ and check'' erased ctx e sinfo = let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in let nerased = DB.set_sink 1 erased in let subst = S.shift 1 in - let hlxp = mkVar ((l, None), 0) dummy_sinfo in + let hlxp = mkVar ((l, None), 0) in let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp nerased in - assert_type nctx d (check nerased nctx d sinfo) - (mkSusp ret (S.shift 2) dummy_sinfo) + assert_type nctx d (check nerased nctx d ) + (mkSusp ret (S.shift 2) ) | None -> if diff > 0 then @@ -844,22 +844,22 @@ and check'' erased ctx e sinfo = let rec indtype fargs start_index = match fargs with | [] -> [] - | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index) dummy_sinfo) + | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index) ) :: indtype fargs (start_index - 1) in let rec fieldargs ftypes = match ftypes with | [] -> let nargs = List.length fieldtypes + List.length fargs in - mkCall (mkSusp t (S.shift nargs) dummy_sinfo, - indtype fargs (nargs - 1)) dummy_sinfo + mkCall (mkSusp t (S.shift nargs) , + indtype fargs (nargs - 1)) | (ak, vd, ftype) :: ftypes -> mkArrow (ak, vd, ftype, lexp_location ftype, - fieldargs ftypes) dummy_sinfo in + fieldargs ftypes) in let rec buildtype fargs = match fargs with | [] -> fieldargs fieldtypes | (_ak, ((l,_) as vd), atype) :: fargs -> mkArrow (P.Aerasable, vd, atype, l, - buildtype fargs) dummy_sinfo in + buildtype fargs) in buildtype fargs with | Not_found @@ -871,9 +871,9 @@ and check'' erased ctx e sinfo = DB.type_int ) | Metavar (idx, s, _) -> (match metavar_lookup idx with - | MVal e -> let e = push_susp e s dummy_sinfo in - check erased ctx e sinfo - | MVar (_, t, _) -> push_susp t s dummy_sinfo) + | MVal e -> let e = push_susp e s in + check erased ctx e + | MVar (_, t, _) -> push_susp t s ) and check' ctx e = let res = check'' DB.set_empty ctx e in @@ -926,7 +926,7 @@ and fv (e : lexp) : (DB.set * mv_set) = | Sort (_, (StypeOmega | StypeLevel)) -> fv_empty | Builtin _ -> fv_empty | Var (_, i) -> (DB.set_singleton i, mv_set_empty) - | Susp (e, s) -> fv (push_susp e s dummy_sinfo) + | Susp (e, s) -> fv (push_susp e s ) | Let (_, defs, e) -> let len = List.length defs in let (fvs, _) @@ -975,9 +975,9 @@ and fv (e : lexp) : (DB.set * mv_set) = cases s | Metavar (id, s, name) -> (match metavar_lookup id with - | MVal e -> fv (push_susp e s dummy_sinfo) + | MVal e -> fv (push_susp e s ) | MVar (sl, t, cl) - -> let (fvs, mvs) = fv_erase (fv (push_susp t s dummy_sinfo)) in + -> let (fvs, mvs) = fv_erase (fv (push_susp t s )) in (fvs, mv_set_add mvs id (sl, t, cl, name))) in let ofvs = LMap.find_opt fv_memo e in @@ -1010,14 +1010,14 @@ and get_type ctx e = | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> DB.type_int | Builtin (_, t) -> t | SortLevel _ -> DB.type_level - | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (mkSLsucc e) dummy_sinfo)) dummy_sinfo + | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (mkSLsucc e) )) | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) -> DB.sort_omega | Var (((_, _name), _idx) as v) -> lookup_type ctx v - | Susp (e, s) -> get_type ctx (push_susp e s dummy_sinfo) + | Susp (e, s) -> get_type ctx (push_susp e s ) | Let (l, defs, e) -> let nctx = DB.lctx_extend_rec ctx defs in - mkSusp (get_type nctx e) (lexp_defs_subst l S.identity defs) dummy_sinfo + mkSusp (get_type nctx e) (lexp_defs_subst l S.identity defs) | Arrow (ak, v, t1, l, t2) (* FIXME: Use `check` here but silencing errors? *) @@ -1026,18 +1026,18 @@ and get_type ctx e = let k2 = get_type nctx t2 in match sort_compose ctx nctx l ak k1 k2 with | SortResult k -> k - | _ -> mkSort (l, StypeOmega) dummy_sinfo) + | _ -> mkSort (l, StypeOmega) ) | Lambda (ak, ((l,_) as v), t, e) -> (mkArrow (ak, v, t, l, get_type (DB.lctx_extend ctx v Variable t) - e) dummy_sinfo) + e) ) | Call (f, args) -> let ft = get_type ctx f in List.fold_left (fun ft (_ak,arg) -> match lexp'_whnf ft ctx with | Arrow (_ak', _v, _t1, _l, t2) - -> mkSusp t2 (S.substitute arg) dummy_sinfo + -> mkSusp t2 (S.substitute arg) | _ -> ft) ft args | Inductive (l, _label, args, cases) @@ -1059,18 +1059,18 @@ and get_type ctx e = -> mkSLlub ctx level (* We need to unshift because the final type * cannot refer to the fields! *) - (mkSusp level' (L.sunshift n) dummy_sinfo) + (mkSusp level' (L.sunshift n) ) | _tt -> level), DB.lctx_extend ictx v Variable t, n + 1)) (level, ctx, 0) case in level) - cases (mkSortLevel SLz dummy_sinfo) in - mkSort (l, Stype level) dummy_sinfo + cases (mkSortLevel SLz ) in + mkSort (l, Stype level) | (ak, v, t)::args -> mkArrow (ak, v, t, lexp_location t, - arg_loop args (DB.lctx_extend ctx v Variable t)) dummy_sinfo in + arg_loop args (DB.lctx_extend ctx v Variable t)) in let tct = arg_loop args ctx in tct | Case (_l, _e, ret, _branches, _default) -> ret @@ -1082,29 +1082,29 @@ and get_type ctx e = let rec indtype fargs start_index = match fargs with | [] -> [] - | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index) dummy_sinfo) + | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index) ) :: indtype fargs (start_index - 1) in let rec fieldargs ftypes = match ftypes with | [] -> let nargs = List.length fieldtypes + List.length fargs in - mkCall (mkSusp t (S.shift nargs) dummy_sinfo, - indtype fargs (nargs - 1)) dummy_sinfo + mkCall (mkSusp t (S.shift nargs) , + indtype fargs (nargs - 1)) | (ak, vd, ftype) :: ftypes -> mkArrow (ak, vd, ftype, lexp_location ftype, - fieldargs ftypes) dummy_sinfo in + fieldargs ftypes) in let rec buildtype fargs = match fargs with | [] -> fieldargs fieldtypes | (_ak, ((l,_) as vd), atype) :: fargs -> mkArrow (P.Aerasable, vd, atype, l, - buildtype fargs) dummy_sinfo in + buildtype fargs) in buildtype fargs with Not_found -> DB.type_int ) | _ -> DB.type_int ) | Metavar (idx, s, _) -> (match metavar_lookup idx with - | MVal e -> get_type ctx (push_susp e s dummy_sinfo) - | MVar (_, t, _) -> push_susp t s dummy_sinfo) + | MVal e -> get_type ctx (push_susp e s ) + | MVar (_, t, _) -> push_susp t s ) (* FIXME: Remove the mutual recursion between `lexp_whnf` and `get_type`, and move this closer to the `lexp_whnf`. *) @@ -1149,7 +1149,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = | L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s) | L.Lambda (P.Aerasable, _, _, body) - -> erase_type lctx (L.push_susp body (S.substitute erasure_dummy) dummy_sinfo) + -> erase_type lctx (L.push_susp body (S.substitute erasure_dummy) ) | L.Lambda (_, vdef, ty, body) -> let lctx' = DB.lctx_extend lctx vdef Variable ty in @@ -1167,7 +1167,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = let ebranches = clean_branch_map lctx branches in E.Case (location, etarget, ebranches, clean_default lctx default) - | L.Susp (l, s) -> erase_type lctx (L.push_susp l s dummy_sinfo) + | L.Susp (l, s) -> erase_type lctx (L.push_susp l s ) (* To be thrown out *) | L.Arrow _ -> E.Type lxp @@ -1178,7 +1178,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = | L.Inductive (_, _, _, _) -> E.Type lxp | L.Metavar (idx, s, _) -> (match metavar_lookup idx with - | MVal e -> erase_type lctx (push_susp e s dummy_sinfo) + | MVal e -> erase_type lctx (push_susp e s ) | MVar _ -> Log.internal_error "Metavar in erase_type") and clean_arg lctx = function @@ -1195,7 +1195,7 @@ and clean_decls and clean_default lctx lxp = match lxp with | Some (v, lxp) - -> let lxp' = L.push_susp lxp (S.substitute erasure_dummy) dummy_sinfo in + -> let lxp' = L.push_susp lxp (S.substitute erasure_dummy) in Some (v, erase_type lctx lxp') | None -> None @@ -1209,12 +1209,12 @@ and clean_branch_map lctx cases = | (_, var) :: tl -> (* Keep the variable and sink the substitution. *) let lctx' = DB.lctx_extend lctx var Variable erasure_dummy in - clean_arg_list tl (var :: acc) (ssink dummy_sinfo var subst) lctx' + clean_arg_list tl (var :: acc) (ssink var subst) lctx' | [] -> (List.rev acc, subst, lctx) in let eargs, subst, lctx' = clean_arg_list args [] S.identity lctx in let subst = S.cons erasure_dummy subst in (* Substitute the equality. *) - (l, eargs, erase_type lctx' (L.push_susp expr subst dummy_sinfo)) + (l, eargs, erase_type lctx' (L.push_susp expr subst )) in SMap.map clean_branch cases @@ -1279,16 +1279,16 @@ let ctx2tup ctx nctx = * let-binding i.s.o the tuple * field (which would be both * equivalent and preferable). *) - mkSusp t (S.shift offset) dummy_sinfo)) + mkSusp t (S.shift offset) )) types) - SMap.empty) dummy_sinfo, - cons_label) dummy_sinfo, + SMap.empty) , + cons_label) , List.mapi (fun i (oname, _t) - -> (P.Aimplicit, mkVar (oname, offset - i - 1) dummy_sinfo)) - types) dummy_sinfo + -> (P.Aimplicit, mkVar (oname, offset - i - 1) )) + types) | (DB.CVlet (name, LetDef (_, e), t, _) :: blocs) - -> mkLet (loc, [(name, mkSusp e (S.shift 1) dummy_sinfo, t)], - mk_lets_and_tup blocs ((name, t) :: types)) dummy_sinfo + -> mkLet (loc, [(name, mkSusp e (S.shift 1) , t)], + mk_lets_and_tup blocs ((name, t) :: types)) | (DB.CVfix (defs, _) :: blocs) -> mkLet (loc, defs, mk_lets_and_tup blocs (List.append @@ -1296,7 +1296,7 @@ let ctx2tup ctx nctx = (List.map (fun (oname, _, t) -> (oname, t)) defs)) - types)) dummy_sinfo + types)) | _ -> assert false in mk_lets_and_tup (get_blocs nctx []) [] ===================================== src/positivity.ml ===================================== @@ -108,7 +108,7 @@ and positive' index lexp = | Lexp.Lambda (_, _, _, e) -> positive index e - | Lexp.Susp (e, s) -> positive index (Lexp.push_susp e s dummy_sinfo) + | Lexp.Susp (e, s) -> positive index (Lexp.push_susp e s ) | Lexp.Var _ (* ===================================== src/sexp.ml ===================================== @@ -41,6 +41,8 @@ type token = sexp let epsilon l = Symbol (l, "") let dummy_epsilon = epsilon dummy_location +let dummy_sinfo = epsilon dummy_location + (********************** Sexp tests **********************) let pred_symbol s pred = ===================================== src/unification.ml ===================================== @@ -135,10 +135,10 @@ let common_subset ctx s1 s2 = let o2 = o2 + o2' in (* FIXME: We should check if le1 and le2 are *unifiable* instead! *) if not (le1 = impossible || le1 = impossible) - && OL.conv_p ctx (mkSusp le1 (S.shift o1) dummy_sinfo) (mkSusp le2 (S.shift o2) dummy_sinfo) + && OL.conv_p ctx (mkSusp le1 (S.shift o1) ) (mkSusp le2 (S.shift o2) ) then match loop s1' s2' o1 o2 1 with | S.Identity 1 -> S.Identity o (* Optimization! *) - | s' -> S.Cons (mkVar ((lexp_location le1, None), 0) dummy_sinfo, + | s' -> S.Cons (mkVar ((lexp_location le1, None), 0) , s', o) else loop s1' s2' o1 o2 (o + 1) (* If one of them reached `Identity`, unroll it, knowing that @@ -146,11 +146,11 @@ let common_subset ctx s1 s2 = * Identity 0 = #0 · #1 · #2 ... = #0 · (Identity 1) *) | (S.Cons _, S.Identity o2') - -> loop s1 (S.Cons (mkVar ((U.dummy_location, None), 0) dummy_sinfo, + -> loop s1 (S.Cons (mkVar ((U.dummy_location, None), 0) , S.Identity 1, o2')) o1 o2 o | (S.Identity o1', S.Cons _) - -> loop (S.Cons (mkVar ((U.dummy_location, None), 0) dummy_sinfo, + -> loop (S.Cons (mkVar ((U.dummy_location, None), 0) , S.Identity 1, o1')) s2 o1 o2 o | (S.Identity o1', S.Identity o2') @@ -215,8 +215,8 @@ and unify' (e1: lexp) (e2: lexp) (* Then, we handle metavariables (aka. flexible-flexible and Flexible-Rigid Equations). Reminder: WHNF implies that the metavariables are not already instanciated. *) - | (_, Metavar (idx, s, _)) -> unify_metavar ctx idx s e2' e1' dummy_sinfo - | (Metavar (idx, s, _), _) -> unify_metavar ctx idx s e1' e2' dummy_sinfo + | (_, Metavar (idx, s, _)) -> unify_metavar ctx idx s e2' e1' + | (Metavar (idx, s, _), _) -> unify_metavar ctx idx s e1' e2' (* Otherwise, the equation is rigid-rigid. Let's start with the cases that can leave residuals: 1. Variables, since they could @@ -292,14 +292,14 @@ and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = - metavar , metavar -> inverse subst (try both sides) - metavar , lexp -> inverse subst *) -and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) sinfo +and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) : return_type = let unif idx s lxp = let t = match metavar_lookup idx with | MVal _ -> Log.internal_error "`lexp_whnf` returned an instantiated metavar!!" - | MVar (_, t, _) -> push_susp t s sinfo in - match Inverse_subst.apply_inv_subst lxp s sinfo with + | MVar (_, t, _) -> push_susp t s in + match Inverse_subst.apply_inv_subst lxp s with | exception Inverse_subst.Not_invertible -> log_info "Unification of metavar failed:\n ?[%s]\nAgainst:\n %s\n" @@ -363,12 +363,12 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) sinfo "`lexp_whnf` returned an instantiated metavar!!" | (Some s_inv, MVar (sl, t, clen)) -> let clen' = clen - s_offset s in - let t' = mkSusp t s_inv sinfo in + let t' = mkSusp t s_inv in let newmv = create_metavar_1 sl t' clen' in - let lexp = mkMetavar (newmv, s, name) sinfo in + let lexp = mkMetavar (newmv, s, name) in assert (sl <= clen); assert (sl <= clen'); - assert (OL.conv_p ctx (mkSusp t' s sinfo) t); + assert (OL.conv_p ctx (mkSusp t' s ) t); (* if (OL.conv_p ctx (mkSusp lexp s1) (mkSusp lexp s2)) then * print_string ("common_subset successful:\n " * ^ subst_string s View it on GitLab: https://gitlab.com/monnier/typer/-/commit/967baf8662b4ffbef9e3cdd9abfb12e79… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/967baf8662b4ffbef9e3cdd9abfb12e79… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Avril 2022