Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer
Commits: 16b2a6b5 by Soilih BEN SOILIH at 2021-05-08T17:50:59-06:00 -
- - - - - 9d8bd5d9 by Soilih BEN SOILIH at 2021-05-10T10:31:41-06:00 update the function browse_lexp
- - - - -
3 changed files:
- src/configuration.json - src/elab.ml - src/typer_lsp_server.ml
Changes:
===================================== src/configuration.json ===================================== @@ -1,4 +1,4 @@ { - "path": "/home/soilih/Projet Maitrise/typer", + "path": "/Projet Maitrise/typer", "description" : "this path is the path from where we run Typer to the typer folder. We must change it to make it work !!!" } \ No newline at end of file
===================================== src/elab.ml ===================================== @@ -74,9 +74,12 @@ let json = Yojson.Basic.from_file "../../configuration.json" *) let exec_path = json |> Yojson.Basic.Util.member "path" |> Yojson.Basic.Util.to_string;; *) + + let btl_folder = + let env_var = Sys.getenv "HOME" in try Sys.getenv "TYPER_BUILTINS" - with Not_found -> (*exec_path*) "/home/soilih/Projet Maitrise/typer" ^ "/btl" + with Not_found -> (*exec_path*) env_var ^ "/Projet Maitrise/typer" ^ "/btl"
let fatal = Log.log_fatal ~section:"ELAB" let error = Log.log_error ~section:"ELAB"
===================================== src/typer_lsp_server.ml ===================================== @@ -213,69 +213,44 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list | Sort (l, Stype e) -> (Lexp.mkSort (l, Stype (Lexp.mkSortLevel (SLsucc e))), location) | Sort (_, StypeLevel) -> (Debruijn.sort_omega, location) | Sort (_, StypeOmega) -> (Debruijn.sort_omega, location) - | Builtin (_, t)-> (t, location)(* - | Var (((l, name), idx) as v) -> (Debruijn.lctx_lookup_type ctx v, location) *) + | Builtin (_, t)-> (t, location) + | Var (((l, name), idx) as v) -> (Debruijn.lctx_lookup_type ctx v, location) | Susp (e, s) -> (Lexp.push_susp e s, location) - (* | Let (l, defs, e) -> let _ = List.fold_left (fun ctx (v, _e, t) - -> (let _ = check_type Debruijn.set_empty ctx t in - Debruijn.lctx_extend ctx v ForwardRef t)) + -> (Debruijn.lctx_extend ctx v ForwardRef t)) ctx defs in - let nerased = nerased_let defs erased in - let nctx = Debruijn.lctx_extend_rec ctx defs in (* FIXME: Termination checking! Positivity-checker! *) let _ = List.fold_left (fun n (_v, e, t) - -> assert_type - nctx e - (check (if Debruijn.set_mem (n - 1) nerased - then Debruijn.set_empty - else nerased) - nctx e) - (push_susp t (S.shift n)); - n - 1) + -> n - 1) (List.length defs) defs in - mkSusp (check nerased nctx e) - (lexp_defs_subst l S.identity defs) - *) - (* + (Lexp.mkSusp e (Opslexp.lexp_defs_subst l Subst.identity defs), location) + | Arrow (ak, v, t1, l, t2) - -> (let k1 = check_type erased ctx t1 in + -> ( let nctx = Debruijn.lexp_ctx_cons ctx v Variable t1 in - let k2 = check_type (Debruijn.set_sink 1 erased) nctx t2 in - match sort_compose ctx nctx l ak k1 k2 with - | SortResult k -> k + match Opslexp.sort_compose ctx nctx l ak t1 t2 with + | SortResult k -> (k, location) | SortInvalid - -> mkSort (l, StypeOmega) + -> (Lexp.mkSort (l, StypeOmega), location) | SortK1NotType - -> mkSort (l, StypeOmega)) + -> (Lexp.mkSort (l, StypeOmega), location) | SortK2NotType - -> mkSort (l, StypeOmega) - | Lambda (ak, ((l,_) as v), t, e) -> (Lexp.mkArrow (ak, v, t, l, - Opslexp.get_type (Debruijn.lctx_extend ctx v Variable t) - e)); - (e,location) - + -> (Lexp.mkSort (l, StypeOmega), location) + ) + | Lambda (ak, ((l,_) as v), t, e) -> (Lexp.mkArrow (ak, v, t, l,e), location) + | Call (f, args) - -> let ft = check erased ctx f in - List.fold_left + -> ((List.fold_left (fun ft (ak,arg) - -> let at = check (if ak = P.Aerasable then Debruijn.set_empty else erased) - ctx arg in - match lexp'_whnf ft ctx with + -> match Opslexp.lexp'_whnf ft ctx with | Arrow (ak', _v, t1, _l, t2) - -> if not (ak == ak') then - (error_tc ~loc:(lexp_location arg) - "arg kind mismatch"; ()) - else (); - assert_type ctx arg at t1; - mkSusp t2 (S.substitute arg) - | _ -> (error_tc ~loc:(lexp_location arg) - ("Calling a non function (type = " - ^ lexp_string ft ^ ")!"); - ft)) - ft args + -> Lexp.mkSusp t2 (Subst.substitute arg) + | _ -> ft + ) + f args), location) + (* | Inductive (l, _label, args, cases) -> let rec arg_loop ctx erased args = match args with @@ -286,43 +261,36 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list 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 + ((let lwhnf = Opslexp.lexp_whnf t ictx in + match Lexp.lexp_lexp' lwhnf with | Sort (_, Stype _) - when ak == P.Aerasable && impredicative_erase + when ak == Pexp.Aerasable -> level | Sort (_, Stype level') - -> mkSLlub ctx level + -> Opslexp.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)) - | _tt -> error_tc ~loc:(lexp_location t) - ~print_action:(fun _ -> - Debruijn.print_lexp_ctx ictx; print_newline () - ) - ("Field type " - ^ lexp_string t - ^ " is not a Type! (" - ^ lexp_string lwhnf ^")"); - level), + (Lexp.mkSusp level' (Lexp.sunshift n)) + | _tt -> level), Debruijn.lctx_extend ictx v Variable t, Debruijn.set_sink 1 erased, n + 1)) (level, ctx, erased, 0) case in level) - cases (mkSortLevel SLz) in - mkSort (l, Stype level) + cases (Lexp.mkSortLevel SLz) in + (Lexp.mkSort (l, Stype level), location) | (ak, v, t)::args - -> let _k = check_type Debruijn.set_empty ctx t in - mkArrow (ak, v, t, lexp_location t, + -> let _k = t in + Lexp.mkArrow (ak, v, t, Lexp.lexp_location t, arg_loop (Debruijn.lctx_extend ctx v Variable t) - (Debruijnset_push ak erased) + (Opslexp.dbset_push ak erased) args) in - let tct = arg_loop ctx erased args in - tct + let tct = arg_loop ctx erased args in + tct + | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) -> let call_split e = @@ -336,7 +304,7 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list let elvl = match lexp'_whnf ekind ctx with | Sort (_, Stype l) -> l | _ -> Log.log_error ~loc:(lexp_location ekind) - "Target lexp's kind is not a sort"; Debruijn.level0 in + "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 | Inductive (_, _, fargs, constructors), aargs -> @@ -354,14 +322,14 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list let tlxp = mkSusp e subst in let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in - let eqty = mkCall (Debruijn.type_eq, + 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)]) in (* Target lexp *) (* The eq proof is erasable. *) - let nerased = Debruijnset_push L.Aerasable nerased in - let nctx = Debruijn.lexp_ctx_cons ctx (l, None) Variable eqty in + let nerased = dbset_push L.Aerasable nerased in + let nctx = DB.lexp_ctx_cons ctx (l, None) Variable eqty in (nerased, nctx) in SMap.iter (fun name (l, vdefs, branch) @@ -372,8 +340,8 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list (* FIXME: If ak is Aerasable, make sure the var only * appears in type annotations. *) | (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes - -> mkctx (Debruijnset_push ak erased) - (Debruijn.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s)) + -> 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))])) vdefs fieldtypes @@ -396,8 +364,8 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list | Some (v, d) -> if diff <= 0 then warning_tc ~loc:l "Redundant default clause"; - let nctx = (Debruijn.lctx_extend ctx v (LetDef (0, e)) etype) in - let nerased = Debruijn.set_sink 1 erased in + 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) in let (nerased, nctx) = @@ -409,41 +377,37 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list error_tc ~loc:l ("Non-exhaustive match: " ^ string_of_int diff ^ " cases missing")) | _,_ -> error_tc ~loc:l "Case on a non-inductive type!"); - ret + ret*) | Cons (t, (_l, name)) - -> (match lexp'_whnf t ctx with + -> (match Opslexp.lexp'_whnf t ctx with | Inductive (l, _, fargs, constructors) -> (try - let fieldtypes = SMap.find name constructors in + let fieldtypes = Util.SMap.find name constructors in let rec indtype fargs start_index = match fargs with | [] -> [] - | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index)) + | (ak, vd, _)::fargs -> (ak, Lexp.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), + Lexp.mkCall (Lexp.mkSusp t (Subst.shift nargs), indtype fargs (nargs - 1)) | (ak, vd, ftype) :: ftypes - -> mkArrow (ak, vd, ftype, lexp_location ftype, + -> Lexp.mkArrow (ak, vd, ftype, Lexp.lexp_location 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, + -> Lexp.mkArrow (Pexp.Aerasable, vd, atype, l, buildtype fargs) in - buildtype fargs + (buildtype fargs, location) with Not_found - -> (error_tc ~loc:l - ("Constructor "" ^ name ^ "" does not exist"); - Debruijn.type_int)) - | _ -> (error_tc ~loc:(lexp_location e) - ("Cons of a non-inductive type: " - ^ lexp_string t); - Debruijn.type_int)) - *) + -> (Debruijn.type_int, location) + ) + | _ -> (Debruijn.type_int, location)) + | Metavar (idx, s, _) -> (match Lexp.metavar_lookup idx with | MVal e -> let e = Lexp.push_susp e s in (e,location) @@ -530,7 +494,7 @@ class lsp_server = let typer_loc = typer_pos_of_lsp_pos pos in let lexp = lexp_search lexp_list typer_loc in let ctx = Elab.default_ectx in - let (l_type,location) = lexp_parcourir ctx lexp in + let (l_type,location) = browse_lexp ctx lexp in let range = lsp_range_of_loc location in let s = Lexp.lexp_string l_type in let r = Lsp.Types.Hover.create
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/ee62886548dc2c7171ff320e9f4c90bad...