Typer
Discussions par mois
- ----- 2026 -----
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2025 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2024 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2023 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2022 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2021 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2020 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2019 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2018 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2017 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2016 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
Décembre 2021
- 1 participants
- 11 discussions
[Git][monnier/typer] Pushed new branch gambit-compiler-pp
by Simon Génier (@ilovemonoids) 30 Déc '21
by Simon Génier (@ilovemonoids) 30 Déc '21
30 Déc '21
Simon Génier pushed new branch gambit-compiler-pp at Stefan / Typer
--
View it on GitLab: https://gitlab.com/monnier/typer/-/tree/gambit-compiler-pp
You're receiving this email because of your account on gitlab.com.
1
0
[Git][monnier/typer][soilih] adding ctx and fixing line numbers in hover
by Soilihi BEN SOILIHI BOINA (@BenSoilih) 27 Déc '21
by Soilihi BEN SOILIHI BOINA (@BenSoilih) 27 Déc '21
27 Déc '21
Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer
Commits:
dd13976d by Soilih BEN SOILIH at 2021-12-26T23:34:06-05:00
adding ctx and fixing line numbers in hover
- - - - -
1 changed file:
- src/typer_lsp_server.ml
Changes:
=====================================
src/typer_lsp_server.ml
=====================================
@@ -837,7 +837,7 @@ let def_loc_search (ctx : Debruijn.lexp_context) (v: vref) =
| [] -> rlst
| ((_, Some s) as vne, _, _)::tl
-> if String.equal s str then
- foo tl (comp + 1) str ((Some (vne,comp))::rlst)
+ foo tl (comp + 1) str ((Some (lctx,vne,comp))::rlst)
else foo tl (comp + 1) str rlst
| _::tl -> foo tl (comp + 1) str rlst
in foo lctx_l 0 str []
@@ -858,23 +858,23 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Loc
| Sort (_, StypeOmega) -> None
| Builtin (_, t) -> None
| Var (vn, idx)
- -> Some (vn,idx)
+ -> Some (ctx, vn,idx)
| Susp (e, s) -> None
| Let (l, defs, e)
-> let ctx' =
List.fold_left (fun ctx (v, _e, t)
-> (Debruijn.lctx_extend ctx v ForwardRef t))
ctx defs in
- let rec foo (ctx_list:Debruijn.env_elem list) cursor comp =
+ let rec foo ctx' (ctx_list:Debruijn.env_elem list) cursor comp =
match ctx_list with
| [] -> failwith "No Variable in the cursor"
| ((l, (Some vn) as v),_,_)::tl
- -> if (vn_on_the_cursor v cursor) then Some (v,comp)
- else foo tl cursor (comp + 1)
- | _::tl -> foo tl cursor (comp + 1)
+ -> if (vn_on_the_cursor v cursor) then Some (ctx',v,comp)
+ else foo ctx' tl cursor (comp + 1)
+ | _::tl -> foo ctx' tl cursor (comp + 1)
in
let ctx_list = Myers.list ctx' in
- foo ctx_list cursor 0
+ foo ctx' ctx_list cursor 0
| Arrow (ak, v, t1, l, t2)
-> None
@@ -1423,7 +1423,14 @@ class lsp_server =
let (l_ctx_r,_,_,_) as ret = browse_lexp lctx lexp typer_loc in
let ret' = (l_ctx_r,None,ltyp,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 location' = {
+ location
+ with
+ start_line = location.start_line - 1;
+ end_line = location.end_line - 1
+ }
+ in
+ let range = lsp_range_of_loc location' in
let s = try use_search_name_in_ctx l_ctx l_type
with exe -> Lexp.lexp_string_for_lsp l_type
in
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/dd13976d45936915f1cd9fb9446af0b22…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/dd13976d45936915f1cd9fb9446af0b22…
You're receiving this email because of your account on gitlab.com.
1
0
Soilihi BEN SOILIHI BOINA pushed to branch add-proj at Stefan / Typer
Commits:
10732224 by Soilih BEN SOILIH at 2021-12-21T23:53:47-05:00
-
- - - - -
1 changed file:
- src/opslexp.ml
Changes:
=====================================
src/opslexp.ml
=====================================
@@ -771,10 +771,9 @@ and check'' erased ctx e =
| [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype
| (ak, (_, Some fn), ftype)::_ when fn = label
(* We found our field! *)
- -> mkSusp ftype s
- (*if ak = Aerasable
- then mkSusp ftype s (* Yay! We found our field! *)
- else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)*)
+ -> if ak = Aerasable
+ then mkSusp ftype s (* Yay! We found our field! *)
+ else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)
| (ak, vdef, ftype)::fieldtypes
-> let fvdef vdef e loc lbl =
match vdef with
@@ -1080,10 +1079,9 @@ and get_type ctx e =
| [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype
| (ak, (_, Some fn), ftype)::_ when fn = label
(* We found our field! *)
- -> mkSusp ftype s
- (*if ak = Aerasable
- then mkSusp ftype s (* Yay! We found our field! *)
- else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)*)
+ -> if ak = Aerasable
+ then mkSusp ftype s (* Yay! We found our field! *)
+ else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)
| (ak, vdef, ftype)::fieldtypes
-> let fvdef vdef e loc lbl =
match vdef with
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/1073222445b85a008370205a875a50b24…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/1073222445b85a008370205a875a50b24…
You're receiving this email because of your account on gitlab.com.
1
0
25 Déc '21
Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer
Commits:
6ff1e63e by Soilih BEN SOILIH at 2021-12-21T06:48:58-05:00
-
- - - - -
42c504dc by Soilih BEN SOILIH at 2021-12-21T20:45:53-05:00
-
- - - - -
3de98c1a by Soilih BEN SOILIH at 2021-12-21T23:24:10-05:00
-
- - - - -
123f4ea2 by Soilih BEN SOILIH at 2021-12-24T19:46:51-05:00
browse_defs
- - - - -
2 changed files:
- src/opslexp.ml
- src/typer_lsp_server.ml
Changes:
=====================================
src/opslexp.ml
=====================================
@@ -772,9 +772,9 @@ and check'' erased ctx e =
| [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype
| (ak, (_, Some fn), ftype)::_ when fn = label
(* We found our field! *)
- -> mkSusp ftype s (*if ak = Aerasable
+ -> if ak = Aerasable
then mkSusp ftype s (* Yay! We found our field! *)
- else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)*)
+ else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)
| (ak, vdef, ftype)::fieldtypes
-> let fvdef vdef e loc lbl =
match vdef with
@@ -1139,9 +1139,9 @@ and get_type ctx e =
| [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype
| (ak, (_, Some fn), ftype)::_ when fn = label
(* We found our field! *)
- -> mkSusp ftype s(*if ak = Aerasable
+ -> if ak = Aerasable
then mkSusp ftype s (* Yay! We found our field! *)
- else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)*)
+ else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)
| (ak, vdef, ftype)::fieldtypes
-> let fvdef vdef e loc lbl =
match vdef with
=====================================
src/typer_lsp_server.ml
=====================================
@@ -42,9 +42,23 @@ open Util
type list_in_list = (vname * Lexp.lexp * Lexp.ltype) list list
type state_after_processing = (log_entry list *
- (list_in_list * Debruijn.elab_context)
+ (list_in_list * Debruijn.elab_context) * ((int * int) option ref)
)
+(*
+let last_pos = ref [(0,0)]
+
+let add_to_tab tab a =
+ if((List.length !tab) > 4) then
+ let l = List.tl(List.rev !tab) in
+ tab := a::(List.rev l)
+ else
+ tab := a::(!tab)
+
+let get_pos_tab tab =
+ List.hd !tab
+*)
+
(* transform a list of logs to a list of tuple
to facilitate the manipulation
*)
@@ -135,14 +149,14 @@ let readstring (str:string) =
let ectx = Elab.default_ectx in
(*let rctx = Elab.default_rctx in*)
let ast = Elab.lexp_decl_str str ectx in
- (!Log.typer_log, ast)
+ (!Log.typer_log, ast, ref None)
let process_some_input_file (_file_contents : string) : state_after_processing =
readstring _file_contents
(*Return the diagnostics of a document state *)
let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list =
- let (log, _) = _state in
+ let (log, _, _) = _state in
let log_tab = log_entry_to_list log in
List.map (fun x ->
let (loc, lev, msg) = x in
@@ -626,11 +640,11 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D
| [] -> ()
| (ak, (_, Some fn), ftype)::_ when fn = label
(* We found our field! *)
- -> if ak = Aerasable
- then
- let a = Lexp.mkSusp ftype s in
- candidats := (browse_lexp ctx a cursor):: !candidats;
- else ()
+ -> if ak = Aerasable
+ then
+ let a = Lexp.mkSusp ftype s in
+ candidats := (browse_lexp ctx a cursor):: !candidats;
+ else failwith "Fail Here!!!"
| (ak, vdef, ftype)::fieldtypes
-> let fvdef vdef e loc lbl =
match vdef with
@@ -805,9 +819,29 @@ let def_loc_search (ctx : Debruijn.lexp_context) (v: vref) =
else tl
|hd::ml::tl -> if (dist hd cursor < dist ml cursor ) then (foo (hd::tl) cursor)
else foo (ml::tl) cursor
-in foo tab cursor
+ in foo tab cursor
+
+ let vn_on_the_cursor (vn:vname) (cursor:location) : bool =
+ let (l,_) = vn in
+ if ((cursor.start_column >= l.start_column)
+ && (cursor.end_column <= l.end_column))
+ then true
+ else false
+
+ let tup_browse_defs_in_ctx (lctx: Debruijn.lexp_context) (vn : vname) =
+ let lctx_l = Myers.list lctx in
+ let (_,so) = vn in
+ let str = Option.get so in
+ let rec foo lst comp str rlst =
+ match lst with
+ | [] -> rlst
+ | ((_, Some s) as vne, _, _)::tl
+ -> if String.equal s str then
+ foo tl (comp + 1) str ((Some (vne,comp))::rlst)
+ else foo tl (comp + 1) str rlst
+ | _::tl -> foo tl (comp + 1) str rlst
+ in foo lctx_l 0 str []
-(*
let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Location.t) =
match Lexp.lexp_lexp' e with
@@ -824,164 +858,42 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Loc
| Sort (_, StypeOmega) -> None
| Builtin (_, t) -> None
| Var (vn, idx)
- -> Some (e,vn,idx)
+ -> Some (vn,idx)
| Susp (e, s) -> None
| Let (l, defs, e)
-> let ctx' =
List.fold_left (fun ctx (v, _e, t)
-> (Debruijn.lctx_extend ctx v ForwardRef t))
ctx defs in
- let rec foo ctx defs cursor ret_list =
- match defs with
- | [] -> ret_list
- | hd::tl -> let (vn,lxp,ltp) = hd in
- foo ctx tl cursor ((browse_defs ctx lxp cursor)::ret_list)
+ let rec foo (ctx_list:Debruijn.env_elem list) cursor comp =
+ match ctx_list with
+ | [] -> failwith "No Variable in the cursor"
+ | ((l, (Some vn) as v),_,_)::tl
+ -> if (vn_on_the_cursor v cursor) then Some (v,comp)
+ else foo tl cursor (comp + 1)
+ | _::tl -> foo tl cursor (comp + 1)
in
- let tab = List.map
- (fun (vn,lxp,ltp) ->
- browse_defs ctx' lxp cursor
- )
- defs
- in
-
- (browse_defs ctx' e cursor)::tab
+ let ctx_list = Myers.list ctx' in
+ foo ctx_list cursor 0
| Arrow (ak, v, t1, l, t2)
- -> (
-
- let (_,_,k1,_) = browse_lexp ctx t1 cursor in
- let nctx = Debruijn.lexp_ctx_cons ctx v Variable t1 in
- let (_,_,k2,_) = browse_lexp nctx t2 cursor in
- match Opslexp.sort_compose ctx nctx l ak k1 k2 with
- | SortResult k -> (nctx, None, k, location)
- | SortInvalid
- -> (nctx, None, Lexp.mkSort (l, StypeOmega), location)
- | SortK1NotType
- -> (nctx, None, Lexp.mkSort (l, StypeOmega), location)
- | SortK2NotType
- -> (nctx, None, Lexp.mkSort (l, StypeOmega), location)
- )
+ -> None
- | Lambda (ak, ((l,_) as v), t, e) -> let ctx' = Debruijn.lctx_extend ctx v Variable t in
- let a = browse_lexp ctx' e cursor in
- let b = browse_lexp ctx t cursor in
- (*let etp = Opslexp.get_type ctx' e in
- let c = (ctx,None, Lexp.mkArrow (ak,v,t,l,etp),l) in*)
- let d = (ctx,None, t,l) in
- browse_list_lexp ([a;b;d]) cursor
+ | Lambda (ak, ((l,_) as v), t, e) -> if (vn_on_the_cursor v cursor) then
+ try List.hd (tup_browse_defs_in_ctx ctx v)
+ with exe -> None
+ else None
- | Call (f, args)
- -> (
- let fonc = browse_lexp ctx f cursor in
- let args_list = List.map
- (fun (_ , e) -> browse_lexp ctx e cursor)
- args
- in
-
- browse_list_lexp (fonc::args_list) cursor
- )
-
- | Inductive (l, _label, args, cases)
- ->
- (
- let rec arg_loop ctx args =
-
- match args with
-
- | []
- -> let (level, tab) =
- SMap.fold
- (fun _ case (level,tab) ->
- let ((level, _, _), tab) =
- List.fold_left
- (
- fun ((level, ictx, n), tab) (ak, v, t) ->
- (
- ((let lwhnf = Opslexp.lexp_whnf (Opslexp.get_type ictx t) ictx in
- match Lexp.lexp_lexp' lwhnf with
- | Sort (_, Stype _)
- when ak == Pexp.Aerasable
- -> level
- | Sort (_, Stype level')
- -> Opslexp.mkSLlub ctx level
- (Lexp.mkSusp level' (Lexp.sunshift n))
- | _tt -> level),
- Debruijn.lctx_extend ictx v Variable t,
- n + 1),
- ((browse_lexp ictx t cursor)::tab)
- )
- )
- ((level, ctx, 0), [] )
- case in
- (level, tab)
- )
- cases
- (Lexp.mkSortLevel SLz, []) in
- browse_list_lexp ((ctx, None,level,l)::tab) cursor
-
- | (ak, v, t)::args
- -> let ctx' = Debruijn.lctx_extend ctx v Variable t in
- browse_list_lexp
- (
- (browse_lexp ctx' t cursor)::(arg_loop ctx' args)::[]
- ) cursor
- in
- arg_loop ctx args
- )
-
- | Proj (l, e, (loc, label))
- -> let candidats = ref [] in
- (
- let call_split (e: Lexp.lexp) =
- match Lexp.lexp_lexp' e with
- | Call (f, args) -> (f, args)
- | _ -> (e,[]) in
- candidats := (browse_lexp ctx e cursor):: !candidats;
- let etype = Opslexp.get_type ctx e in
- let it, aargs = call_split etype in
- match Opslexp.lexp'_whnf it ctx, aargs with
- | Inductive (_, _, fargs, constructors), aargs
- when SMap.cardinal constructors = 1
- -> let rec mksubst s fargs aargs =
- match fargs, aargs with
- | [], [] -> s
- | _farg::fargs, (_ak, aarg)::aargs
- -> mksubst (Subst.cons aarg s) fargs aargs
- | _,_ -> s in
- let s = mksubst Subst.identity fargs aargs in
- let (_,fieldtypes) = List.hd (SMap.bindings constructors) in
- let rec getfieldtype s (fieldtypes : (Pexp.arg_kind * vname * Lexp.ltype) list) =
- match fieldtypes with
- | [] -> ()
- | (ak, (_, Some fn), ftype)::_ when fn = label
- (* We found our field! *)
- -> if ak = Aerasable
- then
- let a = Lexp.mkSusp ftype s in
- candidats := (browse_lexp ctx a cursor):: !candidats;
- else ()
- | (ak, vdef, ftype)::fieldtypes
- -> let fvdef vdef e loc lbl =
- match vdef with
- |(l, Some n) -> Lexp.mkProj (loc, e, lbl)
- |_ -> Lexp.impossible in
- let fieldref = fvdef vdef e l (loc, label) in
- getfieldtype (Subst.cons fieldref s) fieldtypes in
- getfieldtype s fieldtypes; ()
- | Inductive _, _
- -> ()
- | _,_ -> ());
- browse_list_lexp !candidats cursor
-
+ | Call (f, args) -> None
+ | Inductive (l, _label, args, cases) -> None
+ | Proj (l, e, (loc, label)) -> None
| Case (l, e, ret, branches, default)
- ->
- let candidats = ref [] in
-
+ -> let candidats = ref [] in
let call_split (e: Lexp.lexp) =
match Lexp.lexp_lexp' e with
| Call (f, args) -> (f, args)
| _ -> (e,[]) in
- candidats := (browse_lexp ctx e cursor):: !candidats;
+ (* candidats := (browse_lexp ctx e cursor):: !candidats;*)
let etype = Opslexp.get_type ctx e in
(* FIXME save the type in the case lexp instead of recomputing
it over and over again *)
@@ -994,7 +906,7 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Loc
let it, aargs = call_split etype in
(
match Opslexp.lexp'_whnf it ctx, aargs with
-
+
| Inductive (_, _, fargs, constructors), aargs ->
let rec mksubst s fargs aargs =
match fargs, aargs with
@@ -1019,7 +931,7 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Loc
(erased, nctx) in
let brch = SMap.bindings branches in
- let lst =
+ let _ =
List.map
(
fun (name, (l, vdefs, branch))
@@ -1030,7 +942,8 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Loc
(* FIXME: If ak is Aerasable, make sure the var only
* appears in type annotations. *)
| (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes
- -> mkctx (Opslexp.dbset_push ak erased)
+ -> candidats := ((Debruijn.lexp_ctx_cons ctx vdef Variable (Lexp.mkSusp ftype s)), vdef)::!candidats;
+ mkctx (Opslexp.dbset_push ak erased)
(Debruijn.lexp_ctx_cons ctx vdef Variable (Lexp.mkSusp ftype s))
(Lexp.ssink vdef s)
(Lexp.mkCall (Lexp.mkSusp hlxp (Subst.shift 1), [(ak, Lexp.mkVar (vdef, 0))]))
@@ -1042,66 +955,33 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Loc
let (nerased, nctx, hlxp) =
mkctx erased ctx s hctor vdefs fieldtypes in
let subst = Subst.shift (List.length vdefs) in
- let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp in
- candidats := (browse_lexp nctx branch cursor) :: !candidats;
+ ignore(ctx_extend_with_eq nctx subst hlxp)
)
brch
in
-
- let diff = SMap.cardinal constructors - List.length lst in
- (
- match default with
- | Some (v, d)
- -> if diff <= 0 then ();
- let nctx = (Debruijn.lctx_extend ctx v (LetDef (0, e)) etype) in
- let subst = Subst.shift 1 in
- let hlxp = Lexp.mkVar ((l, None), 0) in
- let (_, nctx) =
- ctx_extend_with_eq nctx subst hlxp in
- candidats := (browse_lexp nctx d cursor) :: !candidats;
- ()
- | None
- -> if diff > 0 then (); ()
- )
+ ()
+
+
| _,_ -> () ;
);
- browse_list_lexp !candidats cursor
+ let rec cands (lst: (Debruijn.lexp_context * vname) list) =
+ match lst with
+ | [] -> failwith "No Valid Candidate"
+ | hd::tl -> let (ctx,(l,s)) = hd in
+ if (l.start_column <= cursor.start_column
+ && l.end_column >= cursor.end_column
+ )
+ then hd
+ else cands tl
+ in
+ let (lctx,vn) = cands !candidats in
+ List.hd (tup_browse_defs_in_ctx lctx vn)
+
| Cons (t, (_l, name))
- -> (match Opslexp.lexp'_whnf t ctx with
- | Inductive (l, _, fargs, constructors)
- -> (try
- let fieldtypes = Util.SMap.find name constructors in
- let rec indtype fargs start_index =
- match fargs with
- | [] -> []
- | (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
- Lexp.mkCall (Lexp.mkSusp t (Subst.shift nargs),
- indtype fargs (nargs - 1))
- | (ak, vd, ftype) :: ftypes
- -> 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
- -> Lexp.mkArrow (Pexp.Aerasable, vd, atype, l,
- buildtype fargs) in
- (ctx, None, buildtype fargs, location)
- with Not_found
- -> (ctx, None, Debruijn.type_int, location)
- )
- | _ -> (ctx, None, Debruijn.type_int, location))
-
+ -> None
| Metavar (idx, s, _)
- -> (match Lexp.metavar_lookup idx with
- | MVal e -> let e = Lexp.push_susp e s in
- browse_lexp ctx e cursor
- | MVar (_, t, _) -> (ctx, None, Lexp.push_susp t s, location))
-*)
+ -> None
+
(*==================================Parcourir les définitions==========================*)
(* Search if the vname is in the context *)
@@ -1485,6 +1365,7 @@ class lsp_server =
Lsp.Types.CompletionOptions.create ~triggerCharacters:[ "."; "#"; "\""; "'"; "/"; "@"; "<"]
~resolveProvider:true ()
in
+ (*
let referencesProvider = `Bool true
in
let documentHighlightProvider = `Bool true
@@ -1493,7 +1374,7 @@ class lsp_server =
let documentSymbol =
Lsp.Types.DocumentSymbolOptions.create ~workDoneProgress:true ()
in
-
+ *)
let hoverOption =
Lsp.Types.HoverOptions.create ~workDoneProgress:true ()
in
@@ -1504,16 +1385,17 @@ class lsp_server =
{ arg with Lsp.Types.ServerCapabilities.completionProvider = Some completionProvider ;
Lsp.Types.ServerCapabilities.hoverProvider = Some (`HoverOptions hoverOption);
- Lsp.Types.ServerCapabilities.definitionProvider = Some (`DefinitionOptions definitionOption);
+ Lsp.Types.ServerCapabilities.definitionProvider = Some (`DefinitionOptions definitionOption)(*;
Lsp.Types.ServerCapabilities.referencesProvider = Some referencesProvider ;
Lsp.Types.ServerCapabilities.documentHighlightProvider = Some documentHighlightProvider;
- Lsp.Types.ServerCapabilities.documentSymbolProvider = Some (`DocumentSymbolOptions documentSymbol)
+ Lsp.Types.ServerCapabilities.documentSymbolProvider = Some (`DocumentSymbolOptions documentSymbol)*)
}
method! on_req_definition ~notify_back ~id ~uri ~pos _st =
match Hashtbl.find buffers uri with
- | state_after_processing -> let (_,ast) = state_after_processing in
+ | state_after_processing -> let (_,ast,cur) = state_after_processing in
+ cur := Some (pos.line,pos.character);
let (list_list, _) = ast in
let typer_loc = typer_pos_of_lsp_pos pos in
let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in
@@ -1531,7 +1413,8 @@ class lsp_server =
method! on_req_hover ~notify_back ~id ~uri ~pos doc_state =
match Hashtbl.find buffers uri with
- | state_after_processing -> let (_,ast) = state_after_processing in
+ | state_after_processing -> let (_,ast,cur) = state_after_processing in
+ cur := Some (pos.line,pos.character);
let (list_list, ectx) = ast in
let typer_loc = typer_pos_of_lsp_pos pos in
let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in
@@ -1546,7 +1429,7 @@ class lsp_server =
in
(*let s = Lexp.lexp_string_for_lsp l_type in*)
let r = Lsp.Types.Hover.create
- ~contents:(`MarkedString {Lsp.Types.MarkedString.value=s; language=None})
+ ~contents:(`MarkedString {Lsp.Types.MarkedString.value=s; language=(Some "Typer")})
~range:range ()
in
let e = Some r in
@@ -1556,7 +1439,8 @@ 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) = state_after_processing in
+ | state_after_processing -> let (_,ast,cur) = state_after_processing in
+ cur := Some (pos.line,pos.character);
let (list_list, _) = ast in
let typer_loc = typer_pos_of_lsp_pos pos in
let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in
@@ -1601,7 +1485,7 @@ class lsp_server =
let e = Some (`DocumentSymbol r) in
let f = Linol_lwt.return e in f
-
+
method! on_request_unhandled ~notify_back ~id req =
let f :type r. r Lsp.Client_request.t -> r Linol_lwt.Jsonrpc2.IO.t =
@@ -1643,7 +1527,7 @@ class lsp_server =
| _ -> super#on_request_unhandled ~notify_back ~id req
)
in f req
- *)
+ *)
end
@@ -1654,7 +1538,7 @@ let comp (a:string) (b:string) : string =
else "/*******-----:-(:-(:-(:-(:-(:-(:-(____FAILED___:-(:-(:-(:-(:-(:-(:-(-----*******/\n\n\n"
let hoverTest (ctx:Debruijn.lexp_context) (name:string) (content:string) (position: int * int) (expected:string) =
- let (_, ast) = readstring content in
+ let (_, ast,_) = readstring content in
let (list_list, _) = ast in
let (l,c) = position in
let pos = pos_of_tuple position in
@@ -1796,7 +1680,13 @@ let test () =
hoverTest ctx name "foo x = case x\n\n| true => \"true\"\n\n| false => \"false\" ;" (5,4) "";
hoverTest ctx name "foo x = case x\n\n| true => \"true\"\n\n| false => \"false\" ;" (5,14) ""
-
+
+let time f a b =
+ let t = Sys.time() in
+ let fx = f a b in
+ Printf.printf "Execution time: %fs\n" (Sys.time() -. t);
+ fx
+
(*=======================================Test======================================*)
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/39573a65cce99bb211b653fae49ce64d…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/39573a65cce99bb211b653fae49ce64d…
You're receiving this email because of your account on gitlab.com.
1
0
21 Déc '21
Soilihi BEN SOILIHI BOINA pushed to branch add-proj at Stefan / Typer
Commits:
ec783568 by Soilih BEN SOILIH at 2021-12-21T00:47:24-05:00
fixing...
- - - - -
1 changed file:
- src/opslexp.ml
Changes:
=====================================
src/opslexp.ml
=====================================
@@ -765,15 +765,16 @@ and check'' erased ctx e =
| _,_ -> (log_tc_error ~loc:l
"Wrong arg number to inductive type!"; s) in
let s = mksubst S.identity fargs aargs in
- let fieldtypes = SMap.find label constructors in
+ let (_,fieldtypes) = List.hd (SMap.bindings constructors) in
let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) =
match fieldtypes with
| [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype
| (ak, (_, Some fn), ftype)::_ when fn = label
(* We found our field! *)
- -> if ak = Aerasable
+ -> mkSusp ftype s
+ (*if ak = Aerasable
then mkSusp ftype s (* Yay! We found our field! *)
- else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)
+ else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)*)
| (ak, vdef, ftype)::fieldtypes
-> let fvdef vdef e loc lbl =
match vdef with
@@ -1073,15 +1074,16 @@ and get_type ctx e =
| _,_ -> (log_tc_error ~loc:l
"Wrong arg number to inductive type!"; s) in
let s = mksubst S.identity fargs aargs in
- let fieldtypes = SMap.find label constructors in
+ let (_,fieldtypes) = List.hd (SMap.bindings constructors) in
let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) =
match fieldtypes with
| [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype
| (ak, (_, Some fn), ftype)::_ when fn = label
(* We found our field! *)
- -> if ak = Aerasable
+ -> mkSusp ftype s
+ (*if ak = Aerasable
then mkSusp ftype s (* Yay! We found our field! *)
- else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)
+ else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)*)
| (ak, vdef, ftype)::fieldtypes
-> let fvdef vdef e loc lbl =
match vdef with
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/ec783568fd4831a158f2c0dc0afa836ef…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/ec783568fd4831a158f2c0dc0afa836ef…
You're receiving this email because of your account on gitlab.com.
1
0
21 Déc '21
Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer
Commits:
c5a6a62d by Soilih BEN SOILIH at 2021-12-18T01:30:56-05:00
-
- - - - -
f498d2f1 by Soilih BEN SOILIH at 2021-12-18T13:20:12-05:00
-
- - - - -
39573a65 by Soilih BEN SOILIH at 2021-12-20T21:21:00-05:00
fixing...
- - - - -
4 changed files:
- src/elab.ml
- src/lexp.ml
- src/opslexp.ml
- src/typer_lsp_server.ml
Changes:
=====================================
src/elab.ml
=====================================
@@ -71,17 +71,17 @@ let dloc = dummy_location
let parsing_internals = ref false
let btl_folder =
-
+ (*
let cwd = Sys.getcwd () in
let cdir = String.sub cwd 0 (String.length cwd) in
let canal_entree = open_in (cdir ^ "/.configuration.txt") in
let ligne1 = input_line canal_entree in
let l = String.split_on_char ':' ligne1 in
let m = String.split_on_char '"' (List.nth l 1) in
- let filename = List.nth m 1 in
+ let filename = List.nth m 1 in*)
try Sys.getenv "TYPER_BUILTINS"
- with Not_found -> filename ^ "/btl"
+ with Not_found -> "/home/soilih/Projet Maitrise/typer" (*filename*) ^ "/btl"
let fatal ?print_action ?loc fmt =
Log.log_fatal ~section:"ELAB" ?print_action ?loc fmt
=====================================
src/lexp.ml
=====================================
@@ -530,7 +530,6 @@ let rec lexp_location e =
| Cons (_,(l,_)) -> l
| Case (l,_,_,_,_) -> l
| Susp (e, _) -> lexp_location e
- (* | Susp (_, e) -> lexp_location e *)
| Metavar (_,_,(l,_)) -> l
=====================================
src/opslexp.ml
=====================================
@@ -766,15 +766,15 @@ and check'' erased ctx e =
| _,_ -> (log_tc_error ~loc:l
"Wrong arg number to inductive type!"; s) in
let s = mksubst S.identity fargs aargs in
- let fieldtypes = SMap.find label constructors in
+ let (_,fieldtypes) = List.hd (SMap.bindings constructors) in
let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) =
match fieldtypes with
| [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype
| (ak, (_, Some fn), ftype)::_ when fn = label
(* We found our field! *)
- -> if ak = Aerasable
+ -> mkSusp ftype s (*if ak = Aerasable
then mkSusp ftype s (* Yay! We found our field! *)
- else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)
+ else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)*)
| (ak, vdef, ftype)::fieldtypes
-> let fvdef vdef e loc lbl =
match vdef with
@@ -1133,15 +1133,15 @@ and get_type ctx e =
| _,_ -> (log_tc_error ~loc:l
"Wrong arg number to inductive type!"; s) in
let s = mksubst S.identity fargs aargs in
- let fieldtypes = SMap.find label constructors in
+ let (_,fieldtypes) = List.hd (SMap.bindings constructors) in
let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) =
match fieldtypes with
| [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype
| (ak, (_, Some fn), ftype)::_ when fn = label
(* We found our field! *)
- -> if ak = Aerasable
+ -> mkSusp ftype s(*if ak = Aerasable
then mkSusp ftype s (* Yay! We found our field! *)
- else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)
+ else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)*)
| (ak, vdef, ftype)::fieldtypes
-> let fvdef vdef e loc lbl =
match vdef with
=====================================
src/typer_lsp_server.ml
=====================================
@@ -94,24 +94,6 @@ let lsp_pos_of_pos_end_for_symbol (p:Source.Location.t) : Lsp.Types.Position.t =
let lsp_range_of_loc_for_symbol (l:Source.Location.t) : Lsp.Types.Range.t =
Lsp.Types.Range.create ~start:(lsp_pos_of_pos_start_for_symbol l) ~end_:(lsp_pos_of_pos_end_for_symbol l)
-let rec search_a_vname_with_a_given_position (vname_list: Util.vname list) (location : Source.Location.t): Util.vname =
- match vname_list with
- | [] -> let loc = Source.Location.dummy in
- let s = Some "null" in
- (loc,s)
- | hd::tl ->
- let (loc, _) = hd in
- (*
- let file = "position.txt" in
- let oc = open_out file in (* create or truncate file, return channel *)
- Printf.fprintf oc "loc.start_line = %d \n loc.start_column = %d \n location.start_line = %d \n location.start_column = %d \n " loc.start_line loc.start_column location.start_line location.start_column; (* write something *)
- close_out oc; (* flush and close the channel *)
- *)
- if ((loc.start_line - 1) == location.start_line)
- && ((loc.start_column - 1) == location.start_column)
- then hd
- else search_a_vname_with_a_given_position tl location
-
let vname_to_lsp_loc ~(vname: Util.vname) ~uri : Lsp.Types.Location.t =
let (location, _) = vname in
@@ -146,19 +128,6 @@ let rec nearest_lexp_of_the_list (liste : (vname * Lexp.lexp * Lexp.ltype) list)
then (nearest_lexp_of_the_list (hd::tl) cursor)
else nearest_lexp_of_the_list (ml::tl) cursor
-
-
-let rec search_lexp_with_a_location (list_list: list_in_list) (location : Source.Location.t): Lexp.lexp option =
- let tab = List.map (fun x -> let (a,b,c) = List.nth x 0 in (a,b,c)) list_list in
- let lexp_list = List.map (fun x -> let (_,b,_) = x in b ) tab in
- let rec foo (tab:Lexp.lexp list) (loc:Source.Location.t) =
- match tab with
- | [] -> None
- | hd::tl -> let r = Lexp.lexp_location hd in
- if ((r.start_line - 1) == loc.start_line) && ((r.start_column - 1) == loc.start_column) then Some hd
- else foo tl loc
- in
- foo lexp_list location
(*compile a string and return the logs and ast*)
let readstring (str:string) =
@@ -267,6 +236,7 @@ module Compl = struct
| Event -> Lsp.Types.CompletionItemKind.Event
| Operator -> Lsp.Types.CompletionItemKind.Operator
| TypeParameter -> Lsp.Types.CompletionItemKind.TypeParameter
+
(*
let tranform_string (content:string) : (string * int * int) list =
Base.String.split content ~on:'\n' |>
@@ -277,7 +247,7 @@ module Compl = struct
pos+1, (word,line+1,pos-1)) |>
Base.snd) |>
List.concat
- *)
+
let list_filter_by_line (liste: (string * int * int) list) (line:int) : (string * int * int) list =
List.filter (fun (word,w_line,w_column) -> w_line == line) liste
@@ -291,7 +261,7 @@ module Compl = struct
liste
in
word
-
+
let dist_compl (loc1:string * int * int) (loc2:int * int) =
let (_,loc1_sl,loc1_sc) = loc1 in
let (loc2_sl,loc2_sc) = loc2 in
@@ -301,7 +271,8 @@ module Compl = struct
+. (((float_of_int (loc1_sc)) -. (float_of_int (loc2_sc))) ** 2.0 )
)
)
-
+
+
let rec find_the_nearest_compl (liste:(string * int * int) list) (pos:int * int) : string =
match liste with
@@ -312,7 +283,8 @@ module Compl = struct
|hd::ml::tl -> if ((dist_compl hd pos) < (dist_compl ml pos)) then (find_the_nearest_compl (hd::tl) pos)
else find_the_nearest_compl (ml::tl) pos
-
+ *)
+ (*
let match_str (str:string) : Str.regexp =
str
|> Str.quote
@@ -355,6 +327,7 @@ module Compl = struct
Str.string_match reg x.label 0
)
liste
+ *)
end
(*==============completion============================*)
@@ -639,7 +612,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D
let it, aargs = call_split etype in
match Opslexp.lexp'_whnf it ctx, aargs with
| Inductive (_, _, fargs, constructors), aargs
- when SMap.cardinal constructors != 1
+ when SMap.cardinal constructors = 1
-> let rec mksubst s fargs aargs =
match fargs, aargs with
| [], [] -> s
@@ -647,7 +620,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D
-> mksubst (Subst.cons aarg s) fargs aargs
| _,_ -> s in
let s = mksubst Subst.identity fargs aargs in
- let fieldtypes = SMap.find label constructors in
+ let (_,fieldtypes) = List.hd (SMap.bindings constructors) in
let rec getfieldtype s (fieldtypes : (Pexp.arg_kind * vname * Lexp.ltype) list) =
match fieldtypes with
| [] -> ()
@@ -800,20 +773,336 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D
browse_lexp ctx e cursor
| MVar (_, t, _) -> (ctx, None, Lexp.push_susp t s, location))
- let lexp_parcourir ctx e =
- let lctx = Debruijn.ectx_to_lctx ctx in
- let location = Lexp.lexp_location e in
- (Opslexp.get_type lctx e , location)
-
(*====================================Lexp parcourir===================================*)
-(* Verify if there is a varbind *)
-let verify_varbind (env: Debruijn.env_elem) : (int * Lexp.lexp) option =
- let (_,vrbd,_) = env in
- match vrbd with
- | Variable
- | ForwardRef-> None
- | LetDef (idx,lxp) -> Some (idx,lxp)
+(*==================================Parcourir les définitions==========================*)
+let def_loc_search (ctx : Debruijn.lexp_context) (v: vref) =
+ let ((loc, oename), dbi) = v in
+ try
+ let ((l,_),_,_) as ret = Myers.nth dbi ctx in
+ let _ = match (ret, oename) with
+ | (((_, Some name), _, _), Some ename)
+ -> if not (ename = name) then
+ Log.log_fatal
+ ~loc
+ ({|DeBruijn index %d refers to wrong name. |}
+ ^^ {|Expected: "%s" got "%s"|})
+ dbi ename name
+ | _ -> () in
+
+ l
+ with
+ | Not_found
+ -> Log.log_fatal
+ ~loc "DeBruijn index %d of `%s` out of bounds" dbi (Lexp.maybename oename)
+
+ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) =
+ let rec foo tab cursor =
+ match tab with
+ | [] -> failwith "Liste vide!"
+ | [n] -> n
+ | [hd;tl] -> if (dist hd cursor < dist tl cursor ) then hd
+ else tl
+ |hd::ml::tl -> if (dist hd cursor < dist ml cursor ) then (foo (hd::tl) cursor)
+ else foo (ml::tl) cursor
+in foo tab cursor
+
+(*
+let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Location.t) =
+
+ match Lexp.lexp_lexp' e with
+
+ | Imm (Float (_, _))
+ | Imm (Integer (_, _))
+ | Imm (String (_, _)) -> None
+ | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> None
+ | SortLevel SLz -> None
+ | SortLevel (SLsucc e) -> None
+ | SortLevel (SLlub (e1, e2)) -> None
+ | Sort (l, Stype e) -> None
+ | Sort (_, StypeLevel) -> None
+ | Sort (_, StypeOmega) -> None
+ | Builtin (_, t) -> None
+ | Var (vn, idx)
+ -> Some (e,vn,idx)
+ | Susp (e, s) -> None
+ | Let (l, defs, e)
+ -> let ctx' =
+ List.fold_left (fun ctx (v, _e, t)
+ -> (Debruijn.lctx_extend ctx v ForwardRef t))
+ ctx defs in
+ let rec foo ctx defs cursor ret_list =
+ match defs with
+ | [] -> ret_list
+ | hd::tl -> let (vn,lxp,ltp) = hd in
+ foo ctx tl cursor ((browse_defs ctx lxp cursor)::ret_list)
+ in
+ let tab = List.map
+ (fun (vn,lxp,ltp) ->
+ browse_defs ctx' lxp cursor
+ )
+ defs
+ in
+
+ (browse_defs ctx' e cursor)::tab
+
+ | Arrow (ak, v, t1, l, t2)
+ -> (
+
+ let (_,_,k1,_) = browse_lexp ctx t1 cursor in
+ let nctx = Debruijn.lexp_ctx_cons ctx v Variable t1 in
+ let (_,_,k2,_) = browse_lexp nctx t2 cursor in
+ match Opslexp.sort_compose ctx nctx l ak k1 k2 with
+ | SortResult k -> (nctx, None, k, location)
+ | SortInvalid
+ -> (nctx, None, Lexp.mkSort (l, StypeOmega), location)
+ | SortK1NotType
+ -> (nctx, None, Lexp.mkSort (l, StypeOmega), location)
+ | SortK2NotType
+ -> (nctx, None, Lexp.mkSort (l, StypeOmega), location)
+ )
+
+ | Lambda (ak, ((l,_) as v), t, e) -> let ctx' = Debruijn.lctx_extend ctx v Variable t in
+ let a = browse_lexp ctx' e cursor in
+ let b = browse_lexp ctx t cursor in
+ (*let etp = Opslexp.get_type ctx' e in
+ let c = (ctx,None, Lexp.mkArrow (ak,v,t,l,etp),l) in*)
+ let d = (ctx,None, t,l) in
+ browse_list_lexp ([a;b;d]) cursor
+
+ | Call (f, args)
+ -> (
+ let fonc = browse_lexp ctx f cursor in
+ let args_list = List.map
+ (fun (_ , e) -> browse_lexp ctx e cursor)
+ args
+ in
+
+ browse_list_lexp (fonc::args_list) cursor
+ )
+
+ | Inductive (l, _label, args, cases)
+ ->
+ (
+ let rec arg_loop ctx args =
+
+ match args with
+
+ | []
+ -> let (level, tab) =
+ SMap.fold
+ (fun _ case (level,tab) ->
+ let ((level, _, _), tab) =
+ List.fold_left
+ (
+ fun ((level, ictx, n), tab) (ak, v, t) ->
+ (
+ ((let lwhnf = Opslexp.lexp_whnf (Opslexp.get_type ictx t) ictx in
+ match Lexp.lexp_lexp' lwhnf with
+ | Sort (_, Stype _)
+ when ak == Pexp.Aerasable
+ -> level
+ | Sort (_, Stype level')
+ -> Opslexp.mkSLlub ctx level
+ (Lexp.mkSusp level' (Lexp.sunshift n))
+ | _tt -> level),
+ Debruijn.lctx_extend ictx v Variable t,
+ n + 1),
+ ((browse_lexp ictx t cursor)::tab)
+ )
+ )
+ ((level, ctx, 0), [] )
+ case in
+ (level, tab)
+ )
+ cases
+ (Lexp.mkSortLevel SLz, []) in
+ browse_list_lexp ((ctx, None,level,l)::tab) cursor
+
+ | (ak, v, t)::args
+ -> let ctx' = Debruijn.lctx_extend ctx v Variable t in
+ browse_list_lexp
+ (
+ (browse_lexp ctx' t cursor)::(arg_loop ctx' args)::[]
+ ) cursor
+ in
+ arg_loop ctx args
+ )
+
+ | Proj (l, e, (loc, label))
+ -> let candidats = ref [] in
+ (
+ let call_split (e: Lexp.lexp) =
+ match Lexp.lexp_lexp' e with
+ | Call (f, args) -> (f, args)
+ | _ -> (e,[]) in
+ candidats := (browse_lexp ctx e cursor):: !candidats;
+ let etype = Opslexp.get_type ctx e in
+ let it, aargs = call_split etype in
+ match Opslexp.lexp'_whnf it ctx, aargs with
+ | Inductive (_, _, fargs, constructors), aargs
+ when SMap.cardinal constructors = 1
+ -> let rec mksubst s fargs aargs =
+ match fargs, aargs with
+ | [], [] -> s
+ | _farg::fargs, (_ak, aarg)::aargs
+ -> mksubst (Subst.cons aarg s) fargs aargs
+ | _,_ -> s in
+ let s = mksubst Subst.identity fargs aargs in
+ let (_,fieldtypes) = List.hd (SMap.bindings constructors) in
+ let rec getfieldtype s (fieldtypes : (Pexp.arg_kind * vname * Lexp.ltype) list) =
+ match fieldtypes with
+ | [] -> ()
+ | (ak, (_, Some fn), ftype)::_ when fn = label
+ (* We found our field! *)
+ -> if ak = Aerasable
+ then
+ let a = Lexp.mkSusp ftype s in
+ candidats := (browse_lexp ctx a cursor):: !candidats;
+ else ()
+ | (ak, vdef, ftype)::fieldtypes
+ -> let fvdef vdef e loc lbl =
+ match vdef with
+ |(l, Some n) -> Lexp.mkProj (loc, e, lbl)
+ |_ -> Lexp.impossible in
+ let fieldref = fvdef vdef e l (loc, label) in
+ getfieldtype (Subst.cons fieldref s) fieldtypes in
+ getfieldtype s fieldtypes; ()
+ | Inductive _, _
+ -> ()
+ | _,_ -> ());
+ browse_list_lexp !candidats cursor
+
+ | Case (l, e, ret, branches, default)
+ ->
+ let candidats = ref [] in
+
+ let call_split (e: Lexp.lexp) =
+ match Lexp.lexp_lexp' e with
+ | Call (f, args) -> (f, args)
+ | _ -> (e,[]) in
+ candidats := (browse_lexp ctx e cursor):: !candidats;
+ let etype = Opslexp.get_type ctx e in
+ (* FIXME save the type in the case lexp instead of recomputing
+ it over and over again *)
+ let ekind = Opslexp.get_type ctx etype in
+ let elvl = match Opslexp.lexp'_whnf ekind ctx with
+ | Sort (_, Stype l) -> l
+ | _ -> Debruijn.level0 in
+ let erased = Debruijn.set_empty in
+
+ let it, aargs = call_split etype in
+ (
+ match Opslexp.lexp'_whnf it ctx, aargs with
+
+ | Inductive (_, _, fargs, constructors), aargs ->
+ let rec mksubst s fargs aargs =
+ match fargs, aargs with
+ | [], [] -> s
+ | _farg::fargs, (_ak, aarg)::aargs
+ (* We don't check aarg's type, because we assume that `check`
+ * returns a valid type. *)
+ -> mksubst (Subst.cons aarg s) fargs aargs
+ | _,_ -> s in
+ let s = mksubst Subst.identity fargs aargs in
+ let ctx_extend_with_eq ctx subst hlxp =
+ let tlxp = Lexp.mkSusp e subst in
+ let tltp = Lexp.mkSusp etype subst in
+ let tlvl = Lexp.mkSusp elvl subst in
+ let eqty = Lexp.mkCall (Debruijn.type_eq,
+ [(Lexp.Aerasable, tlvl); (* Typelevel *)
+ (Lexp.Aerasable, tltp); (* Inductive type *)
+ (Lexp.Anormal, hlxp); (* Lexp of the branch head *)
+ (Lexp.Anormal, tlxp)]) in (* Target lexp *)
+ (* The eq proof is erasable. *)
+ let nctx = Debruijn.lexp_ctx_cons ctx (l, None) Variable eqty in
+ (erased, nctx) in
+
+ let brch = SMap.bindings branches in
+ let lst =
+ List.map
+ (
+ fun (name, (l, vdefs, branch))
+ -> let fieldtypes = SMap.find name constructors in
+ let rec mkctx erased ctx s hlxp vdefs fieldtypes =
+ match vdefs, fieldtypes with
+ | [], [] -> (erased, ctx, hlxp)
+ (* FIXME: If ak is Aerasable, make sure the var only
+ * appears in type annotations. *)
+ | (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes
+ -> mkctx (Opslexp.dbset_push ak erased)
+ (Debruijn.lexp_ctx_cons ctx vdef Variable (Lexp.mkSusp ftype s))
+ (Lexp.ssink vdef s)
+ (Lexp.mkCall (Lexp.mkSusp hlxp (Subst.shift 1), [(ak, Lexp.mkVar (vdef, 0))]))
+ vdefs fieldtypes
+ | _,_ -> (erased, ctx, hlxp) in
+ let hctor =
+ Lexp.mkCall (Lexp.mkCons (it, (l, name)),
+ List.map (fun (_, a) -> (Pexp.Aerasable, a)) aargs) in
+ let (nerased, nctx, hlxp) =
+ mkctx erased ctx s hctor vdefs fieldtypes in
+ let subst = Subst.shift (List.length vdefs) in
+ let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp in
+ candidats := (browse_lexp nctx branch cursor) :: !candidats;
+ )
+ brch
+ in
+
+ let diff = SMap.cardinal constructors - List.length lst in
+ (
+ match default with
+ | Some (v, d)
+ -> if diff <= 0 then ();
+ let nctx = (Debruijn.lctx_extend ctx v (LetDef (0, e)) etype) in
+ let subst = Subst.shift 1 in
+ let hlxp = Lexp.mkVar ((l, None), 0) in
+ let (_, nctx) =
+ ctx_extend_with_eq nctx subst hlxp in
+ candidats := (browse_lexp nctx d cursor) :: !candidats;
+ ()
+ | None
+ -> if diff > 0 then (); ()
+ )
+ | _,_ -> () ;
+ );
+ browse_list_lexp !candidats cursor
+ | Cons (t, (_l, name))
+ -> (match Opslexp.lexp'_whnf t ctx with
+ | Inductive (l, _, fargs, constructors)
+ -> (try
+ let fieldtypes = Util.SMap.find name constructors in
+ let rec indtype fargs start_index =
+ match fargs with
+ | [] -> []
+ | (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
+ Lexp.mkCall (Lexp.mkSusp t (Subst.shift nargs),
+ indtype fargs (nargs - 1))
+ | (ak, vd, ftype) :: ftypes
+ -> 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
+ -> Lexp.mkArrow (Pexp.Aerasable, vd, atype, l,
+ buildtype fargs) in
+ (ctx, None, buildtype fargs, location)
+ with Not_found
+ -> (ctx, None, Debruijn.type_int, location)
+ )
+ | _ -> (ctx, None, Debruijn.type_int, location))
+
+ | Metavar (idx, s, _)
+ -> (match Lexp.metavar_lookup idx with
+ | MVal e -> let e = Lexp.push_susp e s in
+ browse_lexp ctx e cursor
+ | MVar (_, t, _) -> (ctx, None, Lexp.push_susp t s, location))
+*)
+(*==================================Parcourir les définitions==========================*)
(* Search if the vname is in the context *)
let search_name_in_ctx (lctx: Debruijn.lexp_context) (lxp: Lexp.lexp) =
@@ -873,13 +1162,13 @@ let search_the_key (ectx: Debruijn.elab_context) (lxp: Lexp.lexp) : string =
(*====================================Definition===================================*)
-let rec find_def_location (ctx:Debruijn.lexp_context) (ret : Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Source.Location.t) : Source.Location.t =
+let rec find_def_location lctx cursor (ret : Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Source.Location.t) : Source.Location.t =
- let (ctx,vr,_,loc) = ret in
+ let (_,vr,_,_) = ret in
match vr with
- | None -> loc
- | Some v -> let ((l,_),_,_) = Debruijn.lctx_lookup ctx v in
+ | None -> cursor
+ | Some v -> let ((l,_),_,_) = Debruijn.lctx_lookup lctx v in
{l with start_line = (l.start_line - 1); end_line = (l.end_line - 1)}
@@ -888,6 +1177,7 @@ let rec find_def_location (ctx:Debruijn.lexp_context) (ret : Debruijn.lexp_conte
(*=====================================Symbols=====================================*)
+(*
let filter_the_list_list (list_list: (vname * Lexp.lexp * Lexp.lexp) list) : (vname * Lexp.lexp * Lexp.lexp) list =
List.filter ( fun x ->
let ((_,s),_,_) = x in
@@ -918,7 +1208,7 @@ let create_symbols (list_list: list_in_list) : Lsp.Types.DocumentSymbol.t list =
~selectionRange:range
()
) filtred_list
-
+ *)
let kind_bread (e: Lexp.lexp) : Lsp.Types.SymbolKind.t =
let open Elexp in
match Lexp.lexp_lexp' e with
@@ -951,7 +1241,7 @@ let create_breadcrumbs (lst: Debruijn.env_elem list) : Lsp.Types.DocumentSymbol.
(*=====================================End Symbols=================================*)
(*====================================Compl===================================*)
-
+ (*
let lsp_compl_from_var (ret : Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Source.Location.t) : Lsp.Types.CompletionItem.t list =
let (_,vr,_,loc) = ret in
@@ -973,7 +1263,7 @@ let create_breadcrumbs (lst: Debruijn.env_elem list) : Lsp.Types.DocumentSymbol.
~textEdit:textEdit ~detail:detail ()
in
[ci]
-
+
let trans_listlist_by_var (ctx:Debruijn.lexp_context) (list_list:list_in_list) (cursor:Source.Location.t) =
let lst = update_the_context ctx list_list in
let nlst = List.map ( fun x ->
@@ -987,7 +1277,8 @@ let create_breadcrumbs (lst: Debruijn.env_elem list) : Lsp.Types.DocumentSymbol.
| None -> false
| Some v -> true
) nlst
-
+ *)
+
let kind_of_a_lexp (e: Lexp.lexp) : Lsp.Types.CompletionItemKind.t =
let open Elexp in
match Lexp.lexp_lexp' e with
@@ -1229,7 +1520,7 @@ class lsp_server =
let (lctx,vx) = lexp_search ctx list_list typer_loc in
let (_,lexp,_) = vx in
let (l_ctx, idx,_ ,_ ) as ret = browse_lexp lctx lexp typer_loc in
- let loc = find_def_location l_ctx ret in
+ let loc = find_def_location lctx typer_loc ret in
let l = Lsp.Types.Location.create
~uri:uri ~range:(lsp_range_of_loc loc)
in
@@ -1293,7 +1584,7 @@ class lsp_server =
let e = Some (`List comp_list_ret) in
let f = Linol_lwt.return e in f
-
+ (*
method! on_req_symbol ~notify_back ~id ~uri () =
match Hashtbl.find buffers uri with
@@ -1309,6 +1600,7 @@ class lsp_server =
let r = create_breadcrumbs filtred_list in
let e = Some (`DocumentSymbol r) in
let f = Linol_lwt.return e in f
+
method! on_request_unhandled ~notify_back ~id req =
@@ -1351,7 +1643,7 @@ class lsp_server =
| _ -> super#on_request_unhandled ~notify_back ~id req
)
in f req
-
+ *)
end
@@ -1504,23 +1796,7 @@ let test () =
hoverTest ctx name "foo x = case x\n\n| true => \"true\"\n\n| false => \"false\" ;" (5,4) "";
hoverTest ctx name "foo x = case x\n\n| true => \"true\"\n\n| false => \"false\" ;" (5,14) ""
-let testSymbols (content:string) =
- let (_, (list_list,_)) = readstring content in
- (*let res = create_symbols list_list in*)
- let res = take_all_list_el list_list in
- let name = "/home/soilih/Bureau/test/symbol.txt" in
- let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in
- (*
- List.iteri (fun i (x : Lsp.Types.DocumentSymbol.t) ->
- let st = "\n" ^ (string_of_int i) ^ " : " ^ (x.name) ^ "\n" in
- output_string oc st
- ) res;
- *)
- output_string oc (string_of_int (List.length res));
- close_out oc
-
- let testS () =
- testSymbols "multiply x y z = _*_ x y ;"
+
(*=======================================Test======================================*)
@@ -1532,7 +1808,6 @@ let run () =
ignore (Arg.Set Log.lsp_enabled);
Logs.set_level ~all:true (Some Logs.Debug);
(*test ();*)
- (*testS ();*)
let s = new lsp_server in
let server = Linol_lwt.Jsonrpc2.create_stdio s in
let task = Linol_lwt.Jsonrpc2.run server in
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/ded4414a5b81adabe753ff09aa07cd02…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/ded4414a5b81adabe753ff09aa07cd02…
You're receiving this email because of your account on gitlab.com.
1
0
15 Déc '21
Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer
Commits:
2c45ce87 by Soilih BEN SOILIH at 2021-12-02T16:00:03-05:00
config
- - - - -
7080f329 by Soilih BEN SOILIH at 2021-12-05T02:12:52-05:00
add proj to my branch
- - - - -
495a8c88 by Soilih BEN SOILIH at 2021-12-10T10:12:48-05:00
resolve Proj errors
- - - - -
ded4414a by Soilih BEN SOILIH at 2021-12-14T21:27:28-05:00
adding breadcrumbs, highlight and references
- - - - -
12 changed files:
- + .configuration.txt
- btl/pervasive.typer
- − configuration.txt
- src/elab.ml
- src/elexp.ml
- src/eval.ml
- src/inverse_subst.ml
- src/lexp.ml
- src/opslexp.ml
- src/positivity.ml
- src/typer_lsp_server.ml
- src/unification.ml
Changes:
=====================================
.configuration.txt
=====================================
@@ -0,0 +1,3 @@
+"filename":"/home/soilih/Projet Maitrise/typer"
+"description":"this filename is the absolute path from where we run Typer.
+We must change it to make it work !!!"
=====================================
btl/pervasive.typer
=====================================
@@ -426,31 +426,6 @@ BoolMod = (##datacons
Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b));
pair = datacons Pair pair;
-__\.__ =
- let mksel o f =
- let constructor = Sexp_node (Sexp_symbol "##datacons")
- (cons (Sexp_symbol "?")
- (cons (Sexp_symbol "cons")
- nil));
- pattern = Sexp_node constructor
- (cons (Sexp_node (Sexp_symbol "_:=_")
- (cons f (cons (Sexp_symbol "v")
- nil)))
- nil);
- branch = Sexp_node (Sexp_symbol "_=>_")
- (cons pattern (cons (Sexp_symbol "v") nil));
- in Sexp_node (Sexp_symbol "case_")
- (cons (Sexp_node (Sexp_symbol "_|_")
- (cons o (cons branch nil)))
- nil)
- in macro (lambda args
- -> IO_return
- case args
- | cons o tail
- => (case tail
- | cons f _ => mksel o f
- | nil => Sexp_error)
- | nil => Sexp_error);
%% Triplet (tuple with 3 values)
type Triplet (a : Type) (b : Type) (c : Type)
=====================================
configuration.txt deleted
=====================================
@@ -1,2 +0,0 @@
-"filename":"/Projet Maitrise/typer"
-"description":"this filename is the place from where we run Typer. We must change it to make it work !!!"
=====================================
src/elab.ml
=====================================
@@ -72,23 +72,16 @@ let dloc = dummy_location
let parsing_internals = ref false
let btl_folder =
- (*
- (* Read the JSON file *)
- let json = Yojson.Basic.from_file "../configuration.json" in
- let exec_path = json |> Yojson.Basic.Util.member "path" |> Yojson.Basic.Util.to_string in
- *)
-
- (*
- let canal_entree = open_in "../configuration.txt" in
+ let cwd = Sys.getcwd () in
+ let cdir = String.sub cwd 0 (String.length cwd) in
+ let canal_entree = open_in (cdir ^ "/.configuration.txt") in
let ligne1 = input_line canal_entree in
let l = String.split_on_char ':' ligne1 in
let m = String.split_on_char '"' (List.nth l 1) in
let filename = List.nth m 1 in
- *)
-
- let env_var = Sys.getenv "HOME" in
+
try Sys.getenv "TYPER_BUILTINS"
- with Not_found -> env_var ^ (*exec_path*) (*filename*) "/Projet Maitrise/typer" ^ "/btl"
+ with Not_found -> filename ^ "/btl"
let fatal ?print_action ?loc fmt =
Log.log_fatal ~section:"ELAB" ?print_action ?loc fmt
@@ -459,6 +452,7 @@ let meta_to_var ids (e : lexp) =
| Sort (_, (StypeOmega | StypeLevel)) -> e
| Builtin _ -> e
| Var (n,i) -> if i < o then e else mkVar (n, i + count)
+ | Proj (l, lxp, lbl) -> mkProj (l, loop o lxp, lbl)
| Susp (e, s) -> loop o (push_susp e s)
| Let (l, defs, e)
-> let len = List.length defs in
@@ -1756,6 +1750,17 @@ let sform_letin ctx loc sargs ot = match sargs with
| _ -> sexp_error loc "Unrecognized let_in_ expression";
sform_dummy_ret ctx loc
+let sform_proj ctx loc sargs ot =
+ match sargs with
+ | [lxp;(Symbol (loca,str))]
+ -> let (ret,_) = infer lxp ctx in
+ let e = mkProj (loc,ret,(loca,str)) in
+ (e, Lazy)
+ | _ -> sexp_error loc "Unrecognized proj expression";
+ sform_dummy_ret ctx loc
+
+
+
let rec infer_level ctx se : lexp =
match se with
| Symbol (_, "z") -> mkSortLevel SLz
@@ -1876,6 +1881,7 @@ let register_special_forms () =
("datacons", sform_datacons);
("typecons", sform_typecons);
("_:_", sform_hastype);
+ ("__.__", sform_proj);
("lambda_->_", sform_lambda Anormal);
("lambda_=>_", sform_lambda Aimplicit);
("lambda_≡>_", sform_lambda Aerasable);
=====================================
src/elexp.ml
=====================================
@@ -51,6 +51,8 @@ type elexp =
(* A variable reference, using deBruijn indexing. *)
| Var of vref
+ (* A projection *)
+ | Proj of U.location * elexp * int
(* Recursive `let` binding. *)
| Let of U.location * (vname * elexp) list * elexp
@@ -83,6 +85,7 @@ let rec elexp_location e =
match e with
| Imm s -> sexp_location s
| Var ((l,_), _) -> l
+ | Proj (l,_,_) -> l
| Builtin ((l, _)) -> l
| Let (l,_,_) -> l
| Lambda ((l,_),_) -> l
@@ -96,6 +99,7 @@ let elexp_name e =
match e with
| Imm _ -> "Imm"
| Var _ -> "Var"
+ | Proj _ -> "Proj"
| Let _ -> "Let"
| Call _ -> "Call"
| Cons _ -> "Cons"
@@ -136,6 +140,9 @@ and elexp_string lxp =
| Imm(s) -> sexp_string s
| Builtin((_, s)) -> s
| Var((_, s), i) -> L.maybename s ^ "[" ^ string_of_int i ^ "]"
+ | Proj (l,lxp,i)
+ -> "( _._ " ^ elexp_string lxp ^ " " ^ (string_of_int i) ^ " )"
+
| Cons (_, (_, s)) -> "datacons(" ^ s ^")"
| Lambda((_, s), b) -> "lambda " ^ L.maybename s ^ " -> " ^ (elexp_string b)
=====================================
src/eval.ml
=====================================
@@ -463,6 +463,17 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type)
(eval f ctx trace)
(List.map (fun e -> eval e ctx trace) args)
+ (* Proj *)
+ | Proj (loc, e, i)
+ -> let vt = eval' e ctx in
+ (
+ match vt with
+ | Vcons (symbol, vtl) -> List.nth vtl i
+ | _ -> error
+ loc
+ "Connot find a value in position %d \n" i
+ )
+
(* Case *)
| Case (loc, target, pat, dflt)
-> (eval_case ctx trace loc target pat dflt)
=====================================
src/inverse_subst.ml
=====================================
@@ -264,6 +264,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp =
| Sort (_l, (StypeOmega | StypeLevel)) -> e
| Builtin _ -> e
| Var (name, i) -> Lexp.mkVar (name, lookup_inv_subst i s)
+ | Proj (l,lxp,lbl) -> mkProj (l, apply_inv_subst lxp s, lbl)
| Susp (e, s') -> apply_inv_subst (push_susp e s') s
| Let (l, defs, e)
-> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in
=====================================
src/lexp.ml
=====================================
@@ -66,6 +66,7 @@ type ltype = lexp
| Sort of U.location * sort
| Builtin of symbol * ltype
| Var of vref
+ | Proj of U.location * lexp * label
| Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *)
(* This "Let" allows recursion. *)
| Let of U.location * (vname * lexp * ltype) list * lexp
@@ -245,6 +246,10 @@ let lexp'_hash (lp : lexp') =
args)))
| Susp (lp, subst)
-> U.combine_hash 14 (U.combine_hash (lexp_hash lp) (Hashtbl.hash subst))
+ | Proj (l,lxp,lbl)
+ -> U.combine_hash 15 (U.combine_hash (Hashtbl.hash l)
+ (U.combine_hash (Hashtbl.hash lxp) (Hashtbl.hash lbl)))
+
(* Equality function for hash table
* using physical equality for "sub-lexp" and compare for `subst`. *)
@@ -309,6 +314,7 @@ 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 mkProj (l,lxp,lbl) = hc (Proj (l,lxp,lbl))
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))
@@ -329,6 +335,7 @@ let lexp_head e =
| Imm s ->
if e = impossible then "impossible" else "Imm" ^ sexp_string s
| Var _ -> "Var"
+ | Proj _ -> "Proj"
| Let _ -> "let"
| Arrow _ -> "Arrow"
| Lambda _ -> "lambda"
@@ -513,6 +520,7 @@ let rec lexp_location e =
| SortLevel SLz -> U.dummy_location
| Imm s -> sexp_location s
| Var ((l,_),_) -> l
+ | Proj (l,_,_) -> l
| Builtin ((l, _), _) -> l
| Let (l,_,_) -> l
| Arrow (_,_,_,l,_) -> l
@@ -590,6 +598,7 @@ let rec push_susp e s = (* Push a suspension one level down. *)
* in many other cases than just when we bump into a Susp. *)
| Susp (e,s') -> push_susp e (scompose s' s)
| (Var _ | Metavar _) -> nosusp (mkSusp e s)
+ | Proj (l,lxp,lbl) -> mkProj (l, mkSusp lxp s, lbl)
and nosusp e = (* Return `e` with no outermost `Susp`. *)
match lexp_lexp' e with
@@ -653,6 +662,7 @@ let clean e =
| Susp (e, s') -> clean (scompose s' s) e
| Var _ -> if S.identity_p s then e
else clean S.identity (mkSusp e s)
+ | Proj (l,lxp,lbl) -> mkProj (l,(clean s lxp),lbl)
| Metavar (idx, s', name)
-> let s = scompose s' s in
match metavar_lookup idx with
@@ -671,6 +681,10 @@ let rec lexp_unparse lxp =
| Builtin ((l,name), _) -> Symbol (l, "##" ^ name)
(* FIXME: Add a Sexp syntax for debindex references. *)
| Var ((loc, name), _) -> Symbol (loc, maybename name)
+ | Proj (l,lxp,(loc,str) )
+ -> Node (Symbol (l, "__.__"),
+ [(lexp_unparse lxp);(Symbol (loc,str))])
+
| Cons (t, (l, name))
-> Node (sdatacons,
[lexp_unparse t; Symbol (l, name)])
@@ -1003,6 +1017,9 @@ and lexp_str ctx (exp : lexp) : string =
| Var ((_loc, name), idx) -> maybename name ^ (index idx) ;
+ | Proj (l,lxp,(loc,str))
+ -> "( _._ " ^ lexp_str' lxp ^ " " ^ str ^ " )"
+
| Metavar (idx, subst, (_loc, name))
(* print metavar result if any *)
-> (match metavar_lookup idx with
=====================================
src/opslexp.ml
=====================================
@@ -747,6 +747,46 @@ and check'' erased ctx e =
args) in
let tct = arg_loop ctx erased args in
tct
+
+ | Proj (l, e, (loc, label))
+ ->( let call_split e =
+ match lexp_lexp' e with
+ | Call (f, args) -> (f, args)
+ | _ -> (e,[]) in
+ let etype = lexp_whnf (check erased ctx e) ctx in
+ let it, aargs = call_split etype in
+ match lexp'_whnf it ctx, aargs with
+ | Inductive (_, _, fargs, constructors), aargs
+ when SMap.cardinal constructors = 1
+ -> let rec mksubst s fargs aargs =
+ match fargs, aargs with
+ | [], [] -> s
+ | _farg::fargs, (_ak, aarg)::aargs
+ -> mksubst (S.cons aarg s) fargs aargs
+ | _,_ -> (log_tc_error ~loc:l
+ "Wrong arg number to inductive type!"; s) in
+ let s = mksubst S.identity fargs aargs in
+ let fieldtypes = SMap.find label constructors in
+ let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) =
+ match fieldtypes with
+ | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype
+ | (ak, (_, Some fn), ftype)::_ when fn = label
+ (* We found our field! *)
+ -> if ak = Aerasable
+ then mkSusp ftype s (* Yay! We found our field! *)
+ else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)
+ | (ak, vdef, ftype)::fieldtypes
+ -> let fvdef vdef e loc lbl =
+ match vdef with
+ |(l, Some n) -> mkProj (loc, e, lbl)
+ |_ -> Lexp.impossible in
+ let fieldref = fvdef vdef e l (loc, label) in
+ getfieldtype (S.cons fieldref s) fieldtypes in
+ getfieldtype s fieldtypes
+ | Inductive _, _
+ -> Log.log_error ~loc:l "Proj on an inductive type that's not a tuple!"; etype
+ | _,_ -> Log.log_error ~loc:l "Proj on a non-inductive type!" ; etype)
+
| Case (l, e, ret, branches, default)
(* FIXME: Check that the return type isn't TypeLevel. *)
-> let call_split e =
@@ -926,6 +966,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)
+ | Proj (l,lxp,lbl) -> fv lxp
| Susp (e, s) -> fv (push_susp e s)
| Let (_, defs, e)
-> let len = List.length defs in
@@ -1072,6 +1113,47 @@ and get_type ctx e =
arg_loop args (DB.lctx_extend ctx v Variable t)) in
let tct = arg_loop args ctx in
tct
+
+ | Proj (l, e, (loc, label))
+ ->( (*check'' DB.set_empty ctx e*)
+ let call_split e =
+ match lexp_lexp' e with
+ | Call (f, args) -> (f, args)
+ | _ -> (e,[]) in
+ let etype = lexp_whnf (get_type ctx e) ctx in
+ let it, aargs = call_split etype in
+ match lexp'_whnf it ctx, aargs with
+ | Inductive (_, _, fargs, constructors), aargs
+ when SMap.cardinal constructors = 1
+ -> let rec mksubst s fargs aargs =
+ match fargs, aargs with
+ | [], [] -> s
+ | _farg::fargs, (_ak, aarg)::aargs
+ -> mksubst (S.cons aarg s) fargs aargs
+ | _,_ -> (log_tc_error ~loc:l
+ "Wrong arg number to inductive type!"; s) in
+ let s = mksubst S.identity fargs aargs in
+ let fieldtypes = SMap.find label constructors in
+ let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) =
+ match fieldtypes with
+ | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype
+ | (ak, (_, Some fn), ftype)::_ when fn = label
+ (* We found our field! *)
+ -> if ak = Aerasable
+ then mkSusp ftype s (* Yay! We found our field! *)
+ else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype)
+ | (ak, vdef, ftype)::fieldtypes
+ -> let fvdef vdef e loc lbl =
+ match vdef with
+ |(l, Some n) -> mkProj (loc, e, lbl)
+ |_ -> Lexp.impossible in
+ let fieldref = fvdef vdef e l (loc, label) in
+ getfieldtype (S.cons fieldref s) fieldtypes in
+ getfieldtype s fieldtypes
+ | Inductive _, _
+ -> Log.log_error ~loc:l "Proj on an inductive type that's not a tuple!"; etype
+ | _,_ -> Log.log_error ~loc:l "Proj on a non-inductive type!" ; etype)
+
| Case (_l, _e, ret, _branches, _default) -> ret
| Cons (t, (_l, name))
-> (match lexp'_whnf t ctx with
@@ -1140,11 +1222,44 @@ let arity_of_cons
^^ {|because it is not an inductive type: %s|})
name (lexp_string ty)
+let pos_of_label lctx label t : int =
+ let call_split e =
+ match lexp_lexp' e with
+ | Call (f, args) -> (f, args)
+ | _ -> (e,[]) in
+ let it, aargs = call_split t in
+ match lexp'_whnf it lctx, aargs with
+ | Inductive (_, _, fargs, constructors), aargs
+ when SMap.cardinal constructors = 1
+ -> let bindings = SMap.bindings constructors in
+ let find_the_pos label (lst : (string * (arg_kind * vname * ltype) list) list) c =
+ match lst with
+ | [ls] -> let (_,l) = ls in
+ let rec foo label (l : (arg_kind * vname * ltype) list) c =
+ match l with
+ | [] -> failwith "label not found!"
+ | hd::tl -> match hd with
+ | (ak, (loc, Some vn), ltp )
+ -> let (_,st) = label in
+ if (String.equal vn st) then c
+ else foo label tl (c + 1)
+ | _ -> foo label tl (c + 1)
+ in
+ foo label l c
+ | _ -> failwith "More than one element!"
+ in find_the_pos label bindings 0
+ | Inductive _, _
+ -> failwith "Proj on an inductive type that's not a tuple!"
+ | _,_ -> failwith "Proj on a non-inductive type!"
+
let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp =
match lexp_lexp' lxp with
| L.Imm (s) -> E.Imm (s)
| L.Builtin (v, _) -> E.Builtin (v)
| L.Var (v) -> E.Var (v)
+ | L.Proj (l, exp, label)
+ -> let t = get_type lctx exp in
+ E.Proj (l, erase_type lctx exp, pos_of_label lctx label t)
| L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s)
| L.Lambda (P.Aerasable, _, _, body)
=====================================
src/positivity.ml
=====================================
@@ -117,6 +117,8 @@ and positive' index lexp =
*)
-> true
+ | Lexp.Proj _ -> false
+
| Lexp.Case _ | Lexp.Cons _ | Lexp.Let _ | Lexp.Sort _ | Lexp.SortLevel _
(* There are no rules that have these synctactic forms as a conclusion. *)
-> false
=====================================
src/typer_lsp_server.ml
=====================================
@@ -625,8 +625,52 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D
) cursor
in
arg_loop ctx args
-
)
+
+ | Proj (l, e, (loc, label))
+ -> let candidats = ref [] in
+ (
+ let call_split (e: Lexp.lexp) =
+ match Lexp.lexp_lexp' e with
+ | Call (f, args) -> (f, args)
+ | _ -> (e,[]) in
+ candidats := (browse_lexp ctx e cursor):: !candidats;
+ let etype = Opslexp.get_type ctx e in
+ let it, aargs = call_split etype in
+ match Opslexp.lexp'_whnf it ctx, aargs with
+ | Inductive (_, _, fargs, constructors), aargs
+ when SMap.cardinal constructors != 1
+ -> let rec mksubst s fargs aargs =
+ match fargs, aargs with
+ | [], [] -> s
+ | _farg::fargs, (_ak, aarg)::aargs
+ -> mksubst (Subst.cons aarg s) fargs aargs
+ | _,_ -> s in
+ let s = mksubst Subst.identity fargs aargs in
+ let fieldtypes = SMap.find label constructors in
+ let rec getfieldtype s (fieldtypes : (Pexp.arg_kind * vname * Lexp.ltype) list) =
+ match fieldtypes with
+ | [] -> ()
+ | (ak, (_, Some fn), ftype)::_ when fn = label
+ (* We found our field! *)
+ -> if ak = Aerasable
+ then
+ let a = Lexp.mkSusp ftype s in
+ candidats := (browse_lexp ctx a cursor):: !candidats;
+ else ()
+ | (ak, vdef, ftype)::fieldtypes
+ -> let fvdef vdef e loc lbl =
+ match vdef with
+ |(l, Some n) -> Lexp.mkProj (loc, e, lbl)
+ |_ -> Lexp.impossible in
+ let fieldref = fvdef vdef e l (loc, label) in
+ getfieldtype (Subst.cons fieldref s) fieldtypes in
+ getfieldtype s fieldtypes; ()
+ | Inductive _, _
+ -> ()
+ | _,_ -> ());
+ browse_list_lexp !candidats cursor
+
| Case (l, e, ret, branches, default)
->
let candidats = ref [] in
@@ -875,6 +919,35 @@ let create_symbols (list_list: list_in_list) : Lsp.Types.DocumentSymbol.t list =
()
) filtred_list
+let kind_bread (e: Lexp.lexp) : Lsp.Types.SymbolKind.t =
+ let open Elexp in
+ match Lexp.lexp_lexp' e with
+ | Lambda (ak, (l,_), t, e) -> Lsp.Types.SymbolKind.Function
+ | Cons (t, (_l, name)) -> Lsp.Types.SymbolKind.Constructor
+ | _ -> Lsp.Types.SymbolKind.Variable
+
+
+let kind_ (element : Debruijn.env_elem ) : Lsp.Types.SymbolKind.t =
+ let (_,vrb,_) = element in
+ match vrb with
+ | Variable
+ | ForwardRef -> Lsp.Types.SymbolKind.Variable
+ | LetDef (_,lxp) -> kind_bread lxp
+
+let create_breadcrumbs (lst: Debruijn.env_elem list) : Lsp.Types.DocumentSymbol.t list =
+ List.map ( fun x ->
+ let ((l,s),_,_) = x in
+ let range = lsp_range_of_loc_for_symbol l in
+ let nm = Option.get s in
+ Lsp.Types.DocumentSymbol.create
+ ~name:nm
+ ~detail:nm
+ ~kind:(kind_ x)
+ ~range:range
+ ~selectionRange:range
+ ()
+ ) lst
+
(*=====================================End Symbols=================================*)
(*====================================Compl===================================*)
@@ -939,19 +1012,37 @@ let create_symbols (list_list: list_in_list) : Lsp.Types.DocumentSymbol.t list =
| None -> filter_lctx tl ret
| Some _ -> filter_lctx tl (hd::ret)
-
-
+
+ let construct_highlights (lst: Debruijn.env_elem list) : Lsp.Types.DocumentHighlight.t list =
+ List.map ( fun (x: Debruijn.env_elem) ->
+ let ((l,s),_,_) = x in
+ let range = Compl.lsp_range_of_a_tuple
+ (l.start_line,l.start_column) (l.end_line,l.end_column)
+ in
+ Lsp.Types.DocumentHighlight.create ~range:range ()
+ ) lst
+ let construct_references uri (lst: Debruijn.env_elem list) : Lsp.Types.Location.t list =
+ List.map ( fun (x: Debruijn.env_elem) ->
+ let ((l,s),_,_) = x in
+ let range = Compl.lsp_range_of_a_tuple
+ (l.start_line,l.start_column) (l.end_line,l.end_column)
+ in
+ Lsp.Types.Location.create ~uri:uri ~range:range
+ ) lst
(* Transform a context to a list of completion item *)
- let ctx_to_ci_list (lctx : Debruijn.env_elem list) (range:Lsp.Types.Range.t) =
+ let ctx_to_ci_list ctx (lctx : Debruijn.env_elem list) (range:Lsp.Types.Range.t) =
List.map ( fun (x: Debruijn.env_elem) ->
let ((_,s),_,t) = x in
let str = Option.get s in
let label = str in
+ let s = try use_search_name_in_ctx ctx t
+ with exe -> Lexp.lexp_string_for_lsp t
+ in
let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:(str) in
let kind = kind_of_a_varbind x in
let ci = Lsp.Types.CompletionItem.create
~label:label ~kind:kind
- ~textEdit:textEdit ~detail:(Lexp.lexp_string t) ()
+ ~textEdit:textEdit ~detail:s ()
in
ci
@@ -1044,7 +1135,7 @@ let create_symbols (list_list: list_in_list) : Lsp.Types.DocumentSymbol.t list =
*)
class lsp_server =
object(self)
- inherit Linol_lwt.Jsonrpc2.server
+ inherit Linol_lwt.Jsonrpc2.server as super
(* one env per document *)
val buffers: (Lsp.Types.DocumentUri.t, state_after_processing) Hashtbl.t
@@ -1103,6 +1194,10 @@ class lsp_server =
Lsp.Types.CompletionOptions.create ~triggerCharacters:[ "."; "#"; "\""; "'"; "/"; "@"; "<"]
~resolveProvider:true ()
in
+ let referencesProvider = `Bool true
+ in
+ let documentHighlightProvider = `Bool true
+ in
let documentSymbol =
Lsp.Types.DocumentSymbolOptions.create ~workDoneProgress:true ()
@@ -1119,6 +1214,8 @@ class lsp_server =
{ arg with Lsp.Types.ServerCapabilities.completionProvider = Some completionProvider ;
Lsp.Types.ServerCapabilities.hoverProvider = Some (`HoverOptions hoverOption);
Lsp.Types.ServerCapabilities.definitionProvider = Some (`DefinitionOptions definitionOption);
+ Lsp.Types.ServerCapabilities.referencesProvider = Some referencesProvider ;
+ Lsp.Types.ServerCapabilities.documentHighlightProvider = Some documentHighlightProvider;
Lsp.Types.ServerCapabilities.documentSymbolProvider = Some (`DocumentSymbolOptions documentSymbol)
}
@@ -1163,22 +1260,8 @@ class lsp_server =
in
let e = Some r in
let f = Linol_lwt.return e in f
-
- (* provisional, to be done later *)
- method! on_req_execute_command ~notify_back ~id _c _args =
- match _c with
- | "typer" -> let file = "command.txt" in
- let message = _c in (* Write message to file *)
- let oc = open_out file in (* create or truncate file, return channel *)
- Printf.fprintf oc "%s\n" message; (* write something *)
- close_out oc; (* flush and close the channel *)
- let h = Lsp.Types.Command.yojson_of_t
- (Lsp.Types.Command.create ~title:_c ~command:_c () ) in
- let e = Linol_lwt.return h in e
- | _ -> assert false
+
-
- (* provisional, to be done later *)
method! on_req_completion ~notify_back ~id ~uri ~pos ~ctx doc_state =
match Hashtbl.find buffers uri with
@@ -1205,21 +1288,70 @@ class lsp_server =
in
let filtred_list = filter_lctx l_ctx [] in
- let comp_list = ctx_to_ci_list filtred_list range in
+ let comp_list = ctx_to_ci_list l_ctx filtred_list range in
let comp_list_ret = complete_oth word comp_list in
let e = Some (`List comp_list_ret) in
let f = Linol_lwt.return e in f
- (*
+
method! on_req_symbol ~notify_back ~id ~uri () =
match Hashtbl.find buffers uri with
- | state_after_processing -> let (_,(list_list, _)) = state_after_processing in
- let r = create_symbols list_list in
+ | state_after_processing -> let (_,ast) = state_after_processing in
+ let (list_list, _) = ast in
+ let typer_loc = pos_of_tuple (Int.max_int,Int.max_int) in
+ let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in
+ let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in
+ let (_,lexp,_) = vx in
+ let (l_ctx,_,_,_) = browse_lexp lctx lexp typer_loc in
+ let filtred_list = filter_lctx l_ctx [] in
+ let r = create_breadcrumbs filtred_list in
let e = Some (`DocumentSymbol r) in
let f = Linol_lwt.return e in f
- *)
+
+ method! on_request_unhandled ~notify_back ~id req =
+
+ let f :type r. r Lsp.Client_request.t -> r Linol_lwt.Jsonrpc2.IO.t =
+ fun req ->
+
+ (match req with
+ | TextDocumentHighlight params
+ -> (
+ match Hashtbl.find buffers params.textDocument.uri with
+ | state_after_processing
+ -> let (_,ast) = state_after_processing in
+ let (list_list, _) = ast in
+ let typer_loc = pos_of_tuple
+ (params.position.line,params.position.character) in
+ let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in
+ let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in
+ let (_,lexp,_) = vx in
+ let (l_ctx,_,_,_) = browse_lexp lctx lexp typer_loc in
+ let filtred_list = filter_lctx l_ctx [] in
+ let hi = construct_highlights filtred_list in
+ let e = Some hi in
+ let f = Linol_lwt.return e in f)
+ | TextDocumentReferences params
+ -> (
+ match Hashtbl.find buffers params.textDocument.uri with
+ | state_after_processing
+ -> let (_,ast) = state_after_processing in
+ let (list_list, _) = ast in
+ let typer_loc = pos_of_tuple
+ (params.position.line,params.position.character) in
+ let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in
+ let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in
+ let (_,lexp,_) = vx in
+ let (l_ctx,_,_,_) = browse_lexp lctx lexp typer_loc in
+ let filtred_list = filter_lctx l_ctx [] in
+ let hi = construct_references (params.textDocument.uri) filtred_list in
+ let e = Some hi in
+ let f = Linol_lwt.return e in f)
+ | _ -> super#on_request_unhandled ~notify_back ~id req
+ )
+ in f req
+
end
=====================================
src/unification.ml
=====================================
@@ -69,6 +69,7 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with
| Sort (_, (StypeOmega | StypeLevel)) -> false
| Builtin _ -> false
| Var (_, _i) -> false
+ | Proj(_,lxp,_) -> oi lxp
| Susp (_e, _s) -> Log.internal_error "`e` should be \"clean\" here!?"
(* ; oi (push_susp e s) *)
| Let (_, defs, e)
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/9a5b03e0602a39243ff663c7564a634c…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/9a5b03e0602a39243ff663c7564a634c…
You're receiving this email because of your account on gitlab.com.
1
0
10 Déc '21
Soilihi BEN SOILIHI BOINA pushed to branch add-proj at Stefan / Typer
Commits:
5abc3040 by Soilih BEN SOILIH at 2021-12-09T10:29:50-05:00
-
- - - - -
2929ef49 by Soilih BEN SOILIH at 2021-12-10T09:55:17-05:00
+
- - - - -
3 changed files:
- btl/pervasive.typer
- src/elab.ml
- src/opslexp.ml
Changes:
=====================================
btl/pervasive.typer
=====================================
@@ -424,33 +424,7 @@ BoolMod = (##datacons
(_ := Bool) (_ := true) (_ := false);
Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b));
-pair = datacons Pair pair;
-
-__\.__ =
- let mksel o f =
- let constructor = Sexp_node (Sexp_symbol "##__.__")
- (cons (Sexp_symbol "?")
- (cons (Sexp_symbol "cons")
- nil));
- pattern = Sexp_node constructor
- (cons (Sexp_node (Sexp_symbol "_:=_")
- (cons f (cons (Sexp_symbol "v")
- nil)))
- nil);
- branch = Sexp_node (Sexp_symbol "_=>_")
- (cons pattern (cons (Sexp_symbol "v") nil));
- in Sexp_node (Sexp_symbol "case_")
- (cons (Sexp_node (Sexp_symbol "_|_")
- (cons o (cons branch nil)))
- nil)
- in macro (lambda args
- -> IO_return
- case args
- | cons o tail
- => (case tail
- | cons f _ => mksel o f
- | nil => Sexp_error)
- | nil => Sexp_error);
+pair = datacons Pair pair;
%% Triplet (tuple with 3 values)
type Triplet (a : Type) (b : Type) (c : Type)
=====================================
src/elab.ml
=====================================
@@ -1729,12 +1729,12 @@ let sform_letin ctx loc sargs ot = match sargs with
let sform_proj ctx loc sargs ot =
match sargs with
- | [Node (Symbol (l, "__.__"), [lxp;(Symbol (loca,str))])]
+ | [lxp;(Symbol (loca,str))]
-> let (ret,_) = infer lxp ctx in
- let e = mkProj (l,ret,(loca,str)) in
+ let e = mkProj (loc,ret,(loca,str)) in
(e, Lazy)
| _ -> sexp_error loc "Unrecognized proj expression";
- sform_dummy_ret ctx loc
+ sform_dummy_ret ctx loc
let rec infer_level ctx se : lexp =
match se with
=====================================
src/opslexp.ml
=====================================
@@ -756,7 +756,7 @@ and check'' erased ctx e =
let it, aargs = call_split etype in
match lexp'_whnf it ctx, aargs with
| Inductive (_, _, fargs, constructors), aargs
- when SMap.cardinal constructors != 1
+ when SMap.cardinal constructors = 1
-> let rec mksubst s fargs aargs =
match fargs, aargs with
| [], [] -> s
@@ -1064,7 +1064,7 @@ and get_type ctx e =
let it, aargs = call_split etype in
match lexp'_whnf it ctx, aargs with
| Inductive (_, _, fargs, constructors), aargs
- when SMap.cardinal constructors != 1
+ when SMap.cardinal constructors = 1
-> let rec mksubst s fargs aargs =
match fargs, aargs with
| [], [] -> s
@@ -1227,7 +1227,7 @@ let pos_of_label lctx label t : int =
let it, aargs = call_split t in
match lexp'_whnf it lctx, aargs with
| Inductive (_, _, fargs, constructors), aargs
- when SMap.cardinal constructors != 1
+ when SMap.cardinal constructors = 1
-> let bindings = SMap.bindings constructors in
let find_the_pos label (lst : (string * (arg_kind * vname * ltype) list) list) c =
match lst with
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/fd27756b4e6d5c378c070ef5a206a4ac…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/fd27756b4e6d5c378c070ef5a206a4ac…
You're receiving this email because of your account on gitlab.com.
1
0
Soilihi BEN SOILIHI BOINA pushed to branch add-proj at Stefan / Typer
Commits:
fd27756b by Soilih BEN SOILIH at 2021-12-02T16:25:21-05:00
eval
- - - - -
1 changed file:
- src/eval.ml
Changes:
=====================================
src/eval.ml
=====================================
@@ -463,8 +463,16 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type)
(eval f ctx trace)
(List.map (fun e -> eval e ctx trace) args)
(* Proj *)
- | Proj (l, e, i)
- -> eval' e ctx
+ | Proj (loc, e, i)
+ -> let vt = eval' e ctx in
+ (
+ match vt with
+ | Vcons (symbol, vtl) -> List.nth vtl i
+ | _ -> error
+ loc
+ "Connot find a value in position %d \n" i
+ )
+
(* Case *)
| Case (loc, target, pat, dflt)
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/fd27756b4e6d5c378c070ef5a206a4acb…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/fd27756b4e6d5c378c070ef5a206a4acb…
You're receiving this email because of your account on gitlab.com.
1
0
02 Déc '21
Soilihi BEN SOILIHI BOINA pushed to branch add-proj at Stefan / Typer
Commits:
f4662f03 by Soilih BEN SOILIH at 2021-12-02T09:55:19-05:00
+
- - - - -
02545ba2 by Soilih BEN SOILIH at 2021-12-02T14:46:37-05:00
lexp to elexp
- - - - -
4 changed files:
- btl/pervasive.typer
- src/elab.ml
- src/eval.ml
- src/opslexp.ml
Changes:
=====================================
btl/pervasive.typer
=====================================
@@ -428,7 +428,7 @@ pair = datacons Pair pair;
__\.__ =
let mksel o f =
- let constructor = Sexp_node (Sexp_symbol "##datacons")
+ let constructor = Sexp_node (Sexp_symbol "##__.__")
(cons (Sexp_symbol "?")
(cons (Sexp_symbol "cons")
nil));
=====================================
src/elab.ml
=====================================
@@ -1732,7 +1732,7 @@ let sform_proj ctx loc sargs ot =
| [Node (Symbol (l, "__.__"), [lxp;(Symbol (loca,str))])]
-> let (ret,_) = infer lxp ctx in
let e = mkProj (l,ret,(loca,str)) in
- (e, Inferred e)
+ (e, Lazy)
| _ -> sexp_error loc "Unrecognized proj expression";
sform_dummy_ret ctx loc
=====================================
src/eval.ml
=====================================
@@ -462,7 +462,7 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type)
-> eval_call (elexp_location f) f trace
(eval f ctx trace)
(List.map (fun e -> eval e ctx trace) args)
- (* TODO: Proj *)
+ (* Proj *)
| Proj (l, e, i)
-> eval' e ctx
=====================================
src/opslexp.ml
=====================================
@@ -1219,12 +1219,44 @@ let arity_of_cons
^^ {|because it is not an inductive type: %s|})
name (lexp_string ty)
+let pos_of_label lctx label t : int =
+ let call_split e =
+ match lexp_lexp' e with
+ | Call (f, args) -> (f, args)
+ | _ -> (e,[]) in
+ let it, aargs = call_split t in
+ match lexp'_whnf it lctx, aargs with
+ | Inductive (_, _, fargs, constructors), aargs
+ when SMap.cardinal constructors != 1
+ -> let bindings = SMap.bindings constructors in
+ let find_the_pos label (lst : (string * (arg_kind * vname * ltype) list) list) c =
+ match lst with
+ | [ls] -> let (_,l) = ls in
+ let rec foo label (l : (arg_kind * vname * ltype) list) c =
+ match l with
+ | [] -> failwith "label not found!"
+ | hd::tl -> match hd with
+ | (ak, (loc, Some vn), ltp )
+ -> let (_,st) = label in
+ if (String.equal vn st) then c
+ else foo label tl (c + 1)
+ | _ -> foo label tl (c + 1)
+ in
+ foo label l c
+ | _ -> failwith "More than one element!"
+ in find_the_pos label bindings 0
+ | Inductive _, _
+ -> failwith "Proj on an inductive type that's not a tuple!"
+ | _,_ -> failwith "Proj on a non-inductive type!"
+
let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp =
match lexp_lexp' lxp with
| L.Imm (s) -> E.Imm (s)
| L.Builtin (v, _) -> E.Builtin (v)
| L.Var (v) -> E.Var (v)
- | L.Proj (l,lxp,lbl) -> failwith "cannot convert a lexp to elexp"
+ | L.Proj (l, exp, label)
+ -> let t = get_type lctx exp in
+ E.Proj (l, erase_type lctx exp, pos_of_label lctx label t)
| L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s)
| L.Lambda (P.Aerasable, _, _, body)
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/291f6c305760ce184dcf3af611298435…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/291f6c305760ce184dcf3af611298435…
You're receiving this email because of your account on gitlab.com.
1
0