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
Juin 2021
- 3 participants
- 9 discussions
[Git][monnier/typer][soilih] 5 commits: elab_check
by Soilihi BEN SOILIHI BOINA (@BenSoilih) 29 Jui '21
by Soilihi BEN SOILIHI BOINA (@BenSoilih) 29 Jui '21
29 Jui '21
Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer
Commits:
0a79b565 by Soilih BEN SOILIH at 2021-06-16T20:53:17-06:00
elab_check
- - - - -
170bef61 by Soilih BEN SOILIH at 2021-06-17T09:50:42-06:00
-
- - - - -
859393dd by Soilih BEN SOILIH at 2021-06-21T23:54:06-06:00
-
- - - - -
79ab4063 by Soilih BEN SOILIH at 2021-06-22T20:09:28-06:00
-
- - - - -
bb0904ae by Soilih BEN SOILIH at 2021-06-29T15:58:45-06:00
fixing context
- - - - -
7 changed files:
- dune
- src/dune
- src/elab.ml
- src/log.ml
- src/opslexp.ml
- src/typer_lsp_server.ml
- typer.ml
Changes:
=====================================
dune
=====================================
@@ -12,4 +12,4 @@
(promote (until-clean))
(modules debug_util)
(libraries typerlib)
- (modes byte native))
+ (modes byte native))
\ No newline at end of file
=====================================
src/dune
=====================================
@@ -5,4 +5,3 @@
linol linol-lwt
lsp jsonrpc yojson base
))
-
=====================================
src/elab.ml
=====================================
@@ -60,6 +60,9 @@ module Unif = Unification
module OL = Opslexp
module EL = Elexp
+(*boolean used to enable checking*)
+let elab_check = ref false
+
(* dummies *)
let dloc = Source.Location.dummy
@@ -214,24 +217,32 @@ let elab_check_def (ctx : elab_context) var lxp ltype =
)
let ctx_extend (ctx: elab_context) (var : vname) def ltype =
- elab_check_proper_type ctx ltype var;
+ if !elab_check then
+ elab_check_proper_type ctx ltype var
+ else ();
ectx_extend ctx var def ltype
let ctx_define (ctx: elab_context) var lxp ltype =
- elab_check_def ctx var lxp ltype;
+ if !elab_check then
+ elab_check_def ctx var lxp ltype
+ else ();
ectx_extend ctx var (LetDef (0, lxp)) ltype
let ctx_define_rec (ctx: elab_context) decls =
let nctx = ectx_extend_rec ctx decls in
let _ = List.fold_left (fun n (var, _lxp, ltp)
- -> elab_check_proper_type
- nctx (push_susp ltp (S.shift n)) var;
+ -> if !elab_check then
+ elab_check_proper_type
+ nctx (push_susp ltp (S.shift n)) var
+ else ();
n - 1)
(List.length decls)
decls in
let _ = List.fold_left (fun n (var, lxp, ltp)
- -> elab_check_def nctx var lxp
- (push_susp ltp (S.shift n));
+ -> if !elab_check then
+ elab_check_def nctx var lxp
+ (push_susp ltp (S.shift n))
+ else ();
n - 1)
(List.length decls)
decls in
=====================================
src/log.ml
=====================================
@@ -204,16 +204,20 @@ let stop_on_error () =
let count = error_count () in
if (0 < count) then
(
+ if !lsp_enabled then
stop_compilation
("Compiler stopped after: "^(string_of_int count)^" errors\n")
+ else ()
)
let stop_on_warning () =
stop_on_error ();
let count = warning_count () in
if (0 < count) then
(
+ if !lsp_enabled then
stop_compilation
("Compiler stopped after: "^(string_of_int count)^" warnings\n")
+ else ()
)
(* Compiler Internal Debug print *)
let debug_msg expr =
=====================================
src/opslexp.ml
=====================================
@@ -583,22 +583,18 @@ and check'' erased ctx e =
let check = check'' in
let assert_type ctx e t t' =
if conv_p ctx t t' then ()
- else ( if !Log.lsp_enabled then
- (error_tc ~loc:(lexp_location e)
+ else (error_tc ~loc:(lexp_location e)
("Type mismatch for "
^ lexp_string e ^ " : "
^ lexp_string t ^ " != "
- ^ lexp_string t'))
- else ();
+ ^ lexp_string t');
(* Log.internal_error "Type mismatch" *)) in
let check_type erased ctx t =
let s = check erased ctx t in
(match lexp'_whnf s ctx with
| Sort _ -> ()
- | _ -> if !Log.lsp_enabled then
- error_tc ~loc:(lexp_location t)
- ("Not a proper type: " ^ lexp_string t)
- else ()
+ | _ -> error_tc ~loc:(lexp_location t)
+ ("Not a proper type: " ^ lexp_string t)
);
(* FIXME: return the `sort` rather than the surrounding `lexp`! *)
s in
@@ -607,8 +603,7 @@ and check'' erased ctx e =
| Imm (Integer (_, _)) -> DB.type_int
| Imm (String (_, _)) -> DB.type_string
| Imm (Block (_, _) | Symbol _ | Node (_, _))
- -> ( if !Log.lsp_enabled then
- error_tc ~loc:(lexp_location e) "Unsupported immediate value!";
+ -> (error_tc ~loc:(lexp_location e) "Unsupported immediate value!";
DB.type_int)
| SortLevel SLz -> DB.type_level
| SortLevel (SLsucc e)
@@ -638,10 +633,9 @@ and check'' erased ctx e =
(* FIXME: Check recursive references. *)
| Var (((l, name), idx) as v)
-> if DB.set_mem idx erased then
- ( if !Log.lsp_enabled then
error_tc ~loc:l
("Var `" ^ maybename name ^ "`"
- ^ " can't be used here, because it's `erasable`"));
+ ^ " can't be used here, because it's `erasable`");
lookup_type ctx v
| Susp (e, s) -> check erased ctx (push_susp e s)
| Let (l, defs, e)
@@ -672,17 +666,14 @@ and check'' erased ctx e =
match sort_compose ctx nctx l ak k1 k2 with
| SortResult k -> k
| SortInvalid
- -> if !Log.lsp_enabled then
- error_tc ~loc:l "Invalid arrow: inner TypelLevel argument";
+ -> error_tc ~loc:l "Invalid arrow: inner TypelLevel argument";
mkSort (l, StypeOmega)
| SortK1NotType
- -> ( if !Log.lsp_enabled then
- error_tc ~loc:(lexp_location t1)
+ -> ( error_tc ~loc:(lexp_location t1)
"Not a proper type";
mkSort (l, StypeOmega))
| SortK2NotType
- -> ( if !Log.lsp_enabled then
- error_tc ~loc:(lexp_location t2)
+ -> ( error_tc ~loc:(lexp_location t2)
"Not a proper type";
mkSort (l, StypeOmega)))
| Lambda (ak, ((l,_) as v), t, e)
@@ -700,14 +691,12 @@ and check'' erased ctx e =
match lexp'_whnf ft ctx with
| Arrow (ak', _v, t1, _l, t2)
-> if not (ak == ak') then
- ( if !Log.lsp_enabled then
- error_tc ~loc:(lexp_location arg)
- "arg kind mismatch"; ())
- else ();
+ error_tc ~loc:(lexp_location arg)
+ "arg kind mismatch"; ()
+ ;
assert_type ctx arg at t1;
mkSusp t2 (S.substitute arg)
- | _ -> ( if !Log.lsp_enabled then
- error_tc ~loc:(lexp_location arg)
+ | _ -> ( error_tc ~loc:(lexp_location arg)
("Calling a non function (type = "
^ lexp_string ft ^ ")!");
ft))
@@ -734,15 +723,14 @@ and check'' erased ctx e =
(* FIXME: If it does refer,
* we get an ugly error! *)
(mkSusp level' (L.sunshift n))
- | _tt -> if !Log.lsp_enabled then
- (error_tc ~loc:(lexp_location t)
+ | _tt -> error_tc ~loc:(lexp_location t)
~print_action:(fun _ ->
DB.print_lexp_ctx ictx; print_newline ()
)
("Field type "
^ lexp_string t
^ " is not a Type! ("
- ^ lexp_string lwhnf ^")"));
+ ^ lexp_string lwhnf ^")");
level),
DB.lctx_extend ictx v Variable t,
DB.set_sink 1 erased,
@@ -785,8 +773,7 @@ and check'' erased ctx e =
(* We don't check aarg's type, because we assume that `check`
* returns a valid type. *)
-> mksubst (S.cons aarg s) fargs aargs
- | _,_ -> ( if !Log.lsp_enabled then
- error_tc ~loc:l
+ | _,_ -> ( error_tc ~loc:l
"Wrong arg number to inductive type!"; s) in
let s = mksubst S.identity fargs aargs in
let ctx_extend_with_eq ctx subst hlxp nerased =
@@ -816,8 +803,7 @@ and check'' erased ctx e =
(ssink vdef s)
(mkCall (mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))]))
vdefs fieldtypes
- | _,_ -> ( if !Log.lsp_enabled then
- error_tc ~loc:l
+ | _,_ -> ( error_tc ~loc:l
"Wrong number of args to constructor!";
(erased, ctx, hlxp)) in
let hctor =
@@ -835,9 +821,9 @@ and check'' erased ctx e =
(match default with
| Some (v, d)
-> if diff <= 0 then
- ( if !Log.lsp_enabled then
+ (
warning_tc ~loc:l "Redundant default clause"
- else ());
+ );
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
@@ -849,16 +835,12 @@ and check'' erased ctx e =
| None
-> if diff > 0 then
(
- if !Log.lsp_enabled then
- (error_tc ~loc:l ("Non-exhaustive match: "
+ error_tc ~loc:l ("Non-exhaustive match: "
^ string_of_int diff ^ " cases missing")
- )
- else ()
+
)
)
- | _,_ -> if !Log.lsp_enabled then
- error_tc ~loc:l "Case on a non-inductive type!"
- else ()
+ | _,_ -> error_tc ~loc:l "Case on a non-inductive type!"
);
ret
| Cons (t, (_l, name))
@@ -887,12 +869,10 @@ and check'' erased ctx e =
buildtype fargs) in
buildtype fargs
with Not_found
- -> ( if !Log.lsp_enabled then
- error_tc ~loc:l
+ -> ( error_tc ~loc:l
("Constructor \"" ^ name ^ "\" does not exist");
DB.type_int))
- | _ -> ( if !Log.lsp_enabled then
- error_tc ~loc:(lexp_location e)
+ | _ -> ( error_tc ~loc:(lexp_location e)
("Cons of a non-inductive type: "
^ lexp_string t);
DB.type_int))
=====================================
src/typer_lsp_server.ml
=====================================
@@ -36,11 +36,11 @@
Diagnostics includes all the warnings, errors and messages that the processing
of a document are expected to be able to return.
*)
-open Log
+open Log
open Util
type state_after_processing = (log_entry list *
- (((vname * Lexp.lexp * Lexp.ltype) list list * Debruijn.elab_context) option)
+ ((vname * Lexp.lexp * Lexp.ltype) list list * Debruijn.elab_context)
)
let log_entry_to_list (tab:log_entry list) : ((string * int * int * int * int) * log_level * string) list =
List.map (fun x -> let location = Option.get x.loc in
@@ -105,15 +105,8 @@ let readstring (str:string) =
Log.clear_log () ;
let ectx = Elab.default_ectx in
(*let rctx = Elab.default_rctx in*)
- let oast =
- try
- Some (Elab.lexp_decl_str str ectx)
- with
- | Log.Stop_Compilation msg
- | Log.Internal_error msg
- | Log.User_error msg -> None
- in
- (!Log.typer_log, oast)
+ let ast = Elab.lexp_decl_str str ectx in
+ (!Log.typer_log, ast)
let process_some_input_file (_file_contents : string) : state_after_processing =
Logs.err (fun k->k " %s" @@ "TEST TEST TEST");
@@ -159,12 +152,17 @@ module Compl = struct
kind:k
}
+ let lsp_pos_of_a_tuple (a,b) : Lsp.Types.Position.t =
+ Lsp.Types.Position.create ~line:(a) ~character:(b)
+
+ let lsp_range_of_a_tuple (a,b) (x,y) : Lsp.Types.Range.t =
+ Lsp.Types.Range.create ~start:(lsp_pos_of_a_tuple (a,b)) ~end_:(lsp_pos_of_a_tuple (x,y))
let t_from_tuple (tup : (int * string * string * string * k) list) : t list =
List.map (fun x
-> let (id,label,newText,detail,kind) = x in
let ret = {
- id = id;
+ id = id ;
label = label ;
newText = newText ;
detail = detail ;
@@ -181,6 +179,7 @@ module Compl = struct
(1, "add", "add()", "add a element to a list", Method);
(1, "pop", "pop()", "remove a element from a list", Method);
]
+
let createKind (element:t) =
match element.kind with
| Text -> Lsp.Types.CompletionItemKind.Text
@@ -241,20 +240,19 @@ module Compl = struct
let rec complete (str:string) (liste: t list) =
match str with
| "List." -> let lst = List.filter (fun x ->
- Int.equal x.id 1
- )
- liste
- in
- let m = String.split_on_char '.' str in
- complete (List.nth m 1) lst
-
+ Int.equal x.id 1
+ )
+ liste
+ in
+ let m = String.split_on_char '.' str in
+ complete (List.nth m 1) lst
| str -> List.filter (fun x ->
let reg = match_str str in
Str.string_match reg x.label 0
)
liste
- end
+end
(*==============completion============================*)
@@ -271,16 +269,18 @@ module Compl = struct
)
)
- let find_the_nearest_lexp (tab:Lexp.lexp list) (cursor:Source.Location.t) =
- let rec foo tab cursor =
- match tab with
+ let find_the_nearest_lexp (lst:(vname * Lexp.lexp * Lexp.ltype) list list) (cursor:Source.Location.t) =
+ let tab = List.map (fun x -> let (a,b,c) = List.nth x 0 in (a,b,c)) lst in
+ let lexp_list = List.map (fun x -> let (_,b,_) = x in b ) tab in
+ let rec foo lexp_list cursor =
+ match lexp_list with
| [] -> failwith "Liste vide!"
| [n] -> n
| [hd;tl] -> if (dist (Lexp.lexp_location hd) cursor < dist (Lexp.lexp_location tl) cursor ) then hd
else tl
|hd::ml::tl -> if (dist (Lexp.lexp_location hd) cursor < dist (Lexp.lexp_location ml) cursor ) then (foo (hd::tl) cursor)
else foo (ml::tl) cursor
- in foo tab cursor
+ in foo lexp_list cursor
let browse_list_lexp (tab:(Lexp.lexp * Source.Location.t) list) (cursor:Source.Location.t) =
let rec foo tab cursor =
@@ -297,10 +297,12 @@ module Compl = struct
else foo (ml::tl) cursor
in foo tab cursor
- let pos_in_lexp_interval (tab:Lexp.lexp list) (cursor:Source.Location.t) =
+ let pos_in_lexp_interval (lst: (vname * Lexp.lexp * Lexp.ltype) list list) (cursor:Source.Location.t) =
+ let tab = List.map (fun x -> let (a,b,c) = List.nth x 0 in (a,b,c)) lst in
+ let lexp_list = List.map (fun x -> let (_,b,_) = x in b ) tab in
let open Source.Location in
- let rec foo tab cursor =
- match tab with
+ let rec foo lexp_list cursor =
+ match lexp_list with
| [] -> failwith "Liste vide!"
| hd::tl -> let location = Lexp.lexp_location hd in
if ((location.start_line <= cursor.start_line && location.start_column <= cursor.start_column)
@@ -308,11 +310,19 @@ module Compl = struct
(location.end_line >= cursor.end_line && location.end_column >= cursor.end_column))
then hd
else foo tl cursor
- in foo tab cursor
-
- let lexp_search (tab:Lexp.lexp list) (cursor:Source.Location.t) =
- try pos_in_lexp_interval tab cursor
- with exn -> find_the_nearest_lexp tab cursor
+ in foo lexp_list cursor
+
+ let lexp_search (ctx: Debruijn.lexp_context) (lst:(vname * Lexp.lexp * Lexp.ltype) list list) (cursor:Source.Location.t) =
+ let lctx = List.fold_left
+ (fun x y ->
+ Debruijn.lctx_extend_rec x y
+ )
+ ctx lst
+ in
+ let lexp = try pos_in_lexp_interval lst cursor
+ with exn -> find_the_nearest_lexp lst cursor
+ in
+ (lctx,lexp)
(* search the type of a lexp browsing a lexp*)
let rec browse_lexp ctx e cursor =
@@ -360,8 +370,11 @@ module Compl = struct
| SortK2NotType
-> (Lexp.mkSort (l, StypeOmega), location)
)
- | Lambda (ak, ((l,_) as v), t, e) -> let (e',loc) = browse_lexp ctx e cursor in
- (Lexp.mkArrow (ak, v, t, l,e'), loc)
+ | 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 (ret,loc) = browse_list_lexp (a::b::[]) cursor in
+ (Lexp.mkArrow (ak, v, t, l,ret), loc)
| Call (f, args)
-> (
@@ -417,18 +430,18 @@ module Compl = struct
let tct = arg_loop ctx Debruijn.set_empty args in
(tct, location)
)
-
+
| Case (l, e, ret, branches, default)
(* FIXME: Check that the return type isn't TypeLevel. *)
->
(
-
+ let candidats = ref [] in
let call_split (e: Lexp.lexp) =
match Lexp.lexp_lexp' e with
| Call (f, args) -> (f, args)
| _ -> (e,[]) in
- let (e',_) = browse_lexp ctx e cursor in
- let etype = Opslexp.lexp_whnf e' ctx 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
@@ -437,7 +450,8 @@ module Compl = struct
| _ -> Debruijn.level0 in
let erased = Debruijn.set_empty in
let it, aargs = call_split etype in
- (match Opslexp.lexp'_whnf it ctx, aargs with
+
+ match Opslexp.lexp'_whnf it ctx, aargs with
| Inductive (_, _, fargs, constructors), aargs ->
let rec mksubst s fargs aargs =
match fargs, aargs with
@@ -464,7 +478,8 @@ module Compl = struct
let brch = SMap.bindings branches in
let lst =
List.map
- (fun (name, (l, vdefs, branch))
+ (
+ 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
@@ -485,9 +500,7 @@ module Compl = struct
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
- ignore (browse_lexp ctx branch cursor);
- (Lexp.mkSusp ret (Subst.shift ((List.length fieldtypes) + 1)))
-
+ candidats := (browse_lexp ctx branch cursor) :: !candidats;
)
brch
in
@@ -503,13 +516,14 @@ module Compl = struct
let hlxp = Lexp.mkVar ((l, None), 0) in
let (nerased, nctx) =
ctx_extend_with_eq nctx subst hlxp in
+ candidats := (browse_lexp ctx d cursor) :: !candidats;
browse_lexp ctx d cursor
| None
-> if diff > 0 then (); (Lexp.impossible, Source.Location.dummy)
)
- | _,_ -> (Lexp.impossible, Source.Location.dummy) );
+ | _,_ -> (Lexp.impossible, Source.Location.dummy) ;
- (ret,location)
+ browse_list_lexp !candidats cursor
)
@@ -609,7 +623,7 @@ class lsp_server =
match Hashtbl.find buffers uri with
| state_after_processing -> let (_,ast) = state_after_processing in
- let (list_list, _) = Option.get ast in
+ let (list_list, _) = ast in
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 typer_loc = typer_pos_of_lsp_pos pos in
@@ -627,13 +641,11 @@ class lsp_server =
match Hashtbl.find buffers uri with
| state_after_processing -> let (_,ast) = state_after_processing in
- let (list_list, _) = Option.get ast in
- 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 (list_list, _) = ast in
let typer_loc = typer_pos_of_lsp_pos pos in
- let lexp = lexp_search lexp_list typer_loc in
let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in
- let (l_type,location) = browse_lexp ctx lexp typer_loc in
+ let (lctx,lexp) = lexp_search ctx list_list typer_loc in
+ let (l_type,location) = browse_lexp lctx lexp typer_loc in
let range = lsp_range_of_loc location in
let s = Lexp.lexp_string_for_lsp l_type in
let r = Lsp.Types.Hover.create
@@ -677,21 +689,25 @@ class lsp_server =
let fbyline = Compl.list_filter_by_line trans_string (pos.line + 1) in
let word = Compl.list_filter_by_character fbyline ((pos.line + 1),pos.character) in
let typer_loc = typer_pos_of_lsp_pos pos in
- let range = lsp_range_of_loc typer_loc in
+
+ let range = Compl.lsp_range_of_a_tuple
+ (typer_loc.start_line,(typer_loc.end_column - 2 - String.length word))
+ (typer_loc.end_line, typer_loc.end_column)
+ in
let tab_compl = Compl.complete word (Compl.t_from_tuple Compl.exemple_liste) in
let r = List.map (fun (x:Compl.t) ->
- let label = x.label in
- let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:(x.newText) in
- let kind = Compl.createKind x in
- let detail = x.detail in
- let ci = Lsp.Types.CompletionItem.create
- ~label:label ~kind:kind
- ~preselect:(true)
- ~textEdit:textEdit ~detail:detail ()
- in
- ci
+ let label = x.label in
+ let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:(x.newText) in
+ let kind = Compl.createKind x in
+ let detail = x.detail in
+ let ci = Lsp.Types.CompletionItem.create
+ ~label:label ~kind:kind
+ ~textEdit:textEdit ~detail:detail ()
+ in
+ ci
+
) tab_compl in
let e = Some (`List r) in
@@ -713,4 +729,4 @@ let run () =
| exception e ->
let e = Printexc.to_string e in
Printf.eprintf "error: %s\n%!" e;
- exit 1
\ No newline at end of file
+ exit 1
=====================================
typer.ml
=====================================
@@ -31,11 +31,9 @@ let welcome_msg =
let arg_batch = ref false
(*
-booléen utilisé pour démarrer le serveur.
-mis true pour les tests
+boolean used to start the LSP server.
+made true for testing
*)
-
-
let lsp_server = ref true
let arg_files = ref []
@@ -45,7 +43,7 @@ let add_input_file file =
let arg_defs =
[("--batch", Arg.Set arg_batch, "Don't run the interactive loop");
("--lsp", Arg.Set lsp_server, "Enable Typer LSP server");
-
+ ("--check", Arg.Set Elab.elab_check, "Enable internal checking");
("--verbosity",
Arg.String Log.set_typer_log_level_str,
"Set the logging level");
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/8e4c57753af78736d6b0d58946e1a742…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/8e4c57753af78736d6b0d58946e1a742…
You're receiving this email because of your account on gitlab.com.
1
0
Bonjour tout le monde,
J'espère que vous allez bien !
J'ai un petit problème que je n'arrive pas à
fixer là qui commence à me prendre du temps.
En soit, j'ai une référence définie comme suit
dans le fichier typer.ml :
elab_check = ref false
Je veux y accéder depuis le fichier typer_lsp_server.ml
qui est dans src/
Si je fais !Typer.elab_check, il trouve pas le module Typer,
si je rajoute typerlib au fichier dune qui est dans src, ça me dit
qu'il y'a une erreur cyclique. Comment résoudre ce problème ?
Merci beaucoup, bien à vous !
2
1
[Git][monnier/typer][soilih] a better way to complete
by Soilihi BEN SOILIHI BOINA (@BenSoilih) 15 Jui '21
by Soilihi BEN SOILIHI BOINA (@BenSoilih) 15 Jui '21
15 Jui '21
Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer
Commits:
8e4c5775 by Soilih BEN SOILIH at 2021-06-15T07:07:01-06:00
a better way to complete
- - - - -
1 changed file:
- src/typer_lsp_server.ml
Changes:
=====================================
src/typer_lsp_server.ml
=====================================
@@ -152,6 +152,7 @@ module Compl = struct
| TypeParameter
type t = {
+ id:int;
label:string;
newText:string;(*the text the completion will send*)
detail:string;
@@ -159,10 +160,11 @@ module Compl = struct
}
- let t_from_tuple (tup : (string * string * string * k) list) : t list =
+ let t_from_tuple (tup : (int * string * string * string * k) list) : t list =
List.map (fun x
- -> let (label,newText,detail,kind) = x in
+ -> let (id,label,newText,detail,kind) = x in
let ret = {
+ id = id;
label = label ;
newText = newText ;
detail = detail ;
@@ -172,13 +174,13 @@ module Compl = struct
) tup
let exemple_liste = [
- ("lambda", "lambda (pattern) -> pattern ", "define a function", Text);
- ("case", "case scrutinee \n | pattern -> pattern ", "pattern matching", Function);
- ("let", "let_in_ (_=_ x ()) x ", "let...in", Text);
- ("if", " if_then_else_ x \"x is true\" \"x is false\"", "if...condition", Text);
- ("add", "add()", "add a element to a list", Method);
+ (0, "lambda", "lambda (pattern) -> pattern ", "define a function", Text);
+ (0, "case", "case scrutinee \n | pattern -> pattern ", "pattern matching", Function);
+ (0, "let", "let_in_ (_=_ x ()) x ", "let...in", Text);
+ (0, "if", " if_then_else_ x \"x is true\" \"x is false\"", "if...condition", Text);
+ (1, "add", "add()", "add a element to a list", Method);
+ (1, "pop", "pop()", "remove a element from a list", Method);
]
-
let createKind (element:t) =
match element.kind with
| Text -> Lsp.Types.CompletionItemKind.Text
@@ -236,12 +238,16 @@ module Compl = struct
|> Str.regexp
- let complete (str:string) (liste: t list) =
+ let rec complete (str:string) (liste: t list) =
match str with
- | "List." -> List.filter (fun x ->
- String.equal x.label "add"
+ | "List." -> let lst = List.filter (fun x ->
+ Int.equal x.id 1
)
- liste
+ liste
+ in
+ let m = String.split_on_char '.' str in
+ complete (List.nth m 1) lst
+
| str -> List.filter (fun x ->
let reg = match_str str in
Str.string_match reg x.label 0
@@ -682,6 +688,7 @@ class lsp_server =
let detail = x.detail in
let ci = Lsp.Types.CompletionItem.create
~label:label ~kind:kind
+ ~preselect:(true)
~textEdit:textEdit ~detail:detail ()
in
ci
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/8e4c57753af78736d6b0d58946e1a7421…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/8e4c57753af78736d6b0d58946e1a7421…
You're receiving this email because of your account on gitlab.com.
1
0
[Git][monnier/typer][soilih] 2 commits: improve print and log error
by Soilihi BEN SOILIHI BOINA (@BenSoilih) 12 Jui '21
by Soilihi BEN SOILIHI BOINA (@BenSoilih) 12 Jui '21
12 Jui '21
Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer
Commits:
8cc99a68 by Soilih BEN SOILIH at 2021-05-31T23:30:38-06:00
improve print and log error
- - - - -
9abad61f by Soilih BEN SOILIH at 2021-06-12T13:16:16-06:00
completion, readstring, check, log
- - - - -
11 changed files:
- debug_util.ml
- − samples/.#acc.typer
- src/debruijn.ml
- src/debug.ml
- src/dune
- src/elab.ml
- src/lexp.ml
- src/log.ml
- src/opslexp.ml
- src/typer_lsp_server.ml
- typer.ml
Changes:
=====================================
debug_util.ml
=====================================
@@ -91,7 +91,7 @@ let format_dest = ref ""
let write_file = ref false
let mod_ctx name v = let f ctx = ctx := SMap.add name v !ctx in
- f ppctx; f debug_ppctx
+ f ppctx; f (if !Log.lsp_enabled then debug_ppctx else debug_ppctx_for_lsp)
let set_print_type v () = mod_ctx "print_type" (Bool v)
let set_print_index v () = mod_ctx "print_dbi" (Bool v)
=====================================
samples/.#acc.typer deleted
=====================================
@@ -1 +0,0 @@
-soilih@soilih-HP-Laptop-15-db0xxx.11163:1621953914
\ No newline at end of file
=====================================
src/debruijn.ml
=====================================
@@ -292,7 +292,7 @@ let print_lexp_ctx_n (ctx : lexp_context) (ranges : (int * int) list) =
(match lexp with
| None -> print_string "<var>"
| Some lexp
- -> (let str = lexp_str (!debug_ppctx) lexp in
+ -> (let str = lexp_str (if !Log.lsp_enabled then (!debug_ppctx) else (!debug_ppctx_for_lsp)) lexp in
let strs =
match String.split_on_char '\n' str with
| hd :: tl -> print_string hd; tl
=====================================
src/debug.ml
=====================================
@@ -124,7 +124,7 @@ let debug_lexp_decls decls =
lalign_print_string (lexp_name lxp) 15;
Printf.printf "[%s]" (Source.Location.to_string loc);
- let str = lexp_str_decls (!debug_ppctx) [e] in
+ let str = lexp_str_decls (if !Log.lsp_enabled then (!debug_ppctx) else (!debug_ppctx_for_lsp)) [e] in
(* First col size = 15 + 1 + 2 + 3 + 5 + 6
* = 32 *)
=====================================
src/dune
=====================================
@@ -3,6 +3,6 @@
(name typerlib)
(libraries zarith str
linol linol-lwt
- lsp jsonrpc yojson
+ lsp jsonrpc yojson base
))
=====================================
src/elab.ml
=====================================
@@ -187,6 +187,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype =
~loc
"Error while type-checking";
raise e in
+
if (try OL.conv_p (ectx_to_lctx ctx) ltype ltype'
with e ->
info ~print_action:(lexp_print_details lxp)
@@ -198,18 +199,18 @@ let elab_check_def (ctx : elab_context) var lxp ltype =
elab_check_proper_type ctx ltype var
else
(
- if !Log.lsp_enabled then
- fatal
- ~print_action:(fun _ ->
- List.iter print_indent_line [
- (match var with (_, Some n) -> n | _ -> "<anon>")
- ^ " = " ^ lexp_string lxp ^ " !: " ^ lexp_string ltype;
- " because";
- lexp_string ltype' ^ " != " ^ lexp_string ltype
- ])
- ~loc
- "Type check error: ¡¡ctx_define error!!"
- else ()
+ (*if !Log.lsp_enabled then*)
+ (fatal
+ ~print_action:(fun _ ->
+ List.iter print_indent_line [
+ (match var with (_, Some n) -> n | _ -> "<anon>")
+ ^ " = " ^ lexp_string lxp ^ " !: " ^ lexp_string ltype;
+ " because";
+ lexp_string ltype' ^ " != " ^ lexp_string ltype
+ ])
+ ~loc
+ "Type check error: ¡¡ctx_define error!!")
+ (*else ()*)
)
let ctx_extend (ctx: elab_context) (var : vname) def ltype =
=====================================
src/lexp.ml
=====================================
@@ -929,7 +929,7 @@ let rec get_precedence expr ctx =
* ========================================== *)
let rec lexp_print e = print_string (lexp_string e)
-and lexp_string e = lexp_cstring (!debug_ppctx) e
+and lexp_string e = lexp_cstring (if !Log.lsp_enabled then (!debug_ppctx) else (!debug_ppctx_for_lsp)) e
(* Context Print *)
and lexp_cprint ctx e = print_string (lexp_cstring ctx e)
=====================================
src/log.ml
=====================================
@@ -79,8 +79,8 @@ type log_config = {
}
let typer_log_config = {
- level = Warning;
- print_at_log = false;
+ level = Debug;
+ print_at_log = true;
print_in_reverse = false;
color = true;
}
@@ -189,8 +189,9 @@ let stop_compilation s = raise (Stop_Compilation s)
let log_fatal ?section ?print_action ?loc m =
typer_log_config.print_at_log <- true;
+ typer_log_config.level <- Debug;
log_msg Fatal ~kind:"[X] Fatal " ?section ?print_action ?loc m;
- internal_error "Compiler Fatal Error"
+ internal_error (*"Compiler Fatal Error"*) m
@@ -203,20 +204,16 @@ let stop_on_error () =
let count = error_count () in
if (0 < count) then
(
- if !lsp_enabled then
stop_compilation
("Compiler stopped after: "^(string_of_int count)^" errors\n")
- else ()
)
let stop_on_warning () =
stop_on_error ();
let count = warning_count () in
if (0 < count) then
(
- if !lsp_enabled then
stop_compilation
("Compiler stopped after: "^(string_of_int count)^" warnings\n")
- else ()
)
(* Compiler Internal Debug print *)
let debug_msg expr =
=====================================
src/opslexp.ml
=====================================
@@ -583,18 +583,23 @@ and check'' erased ctx e =
let check = check'' in
let assert_type ctx e t t' =
if conv_p ctx t t' then ()
- else (error_tc ~loc:(lexp_location e)
- ("Type mismatch for "
- ^ lexp_string e ^ " : "
- ^ lexp_string t ^ " != "
- ^ lexp_string t');
+ else ( if !Log.lsp_enabled then
+ (error_tc ~loc:(lexp_location e)
+ ("Type mismatch for "
+ ^ lexp_string e ^ " : "
+ ^ lexp_string t ^ " != "
+ ^ lexp_string t'))
+ else ();
(* Log.internal_error "Type mismatch" *)) in
let check_type erased ctx t =
let s = check erased ctx t in
(match lexp'_whnf s ctx with
| Sort _ -> ()
- | _ -> error_tc ~loc:(lexp_location t)
- ("Not a proper type: " ^ lexp_string t));
+ | _ -> if !Log.lsp_enabled then
+ error_tc ~loc:(lexp_location t)
+ ("Not a proper type: " ^ lexp_string t)
+ else ()
+ );
(* FIXME: return the `sort` rather than the surrounding `lexp`! *)
s in
match lexp_lexp' e with
@@ -602,7 +607,8 @@ and check'' erased ctx e =
| Imm (Integer (_, _)) -> DB.type_int
| Imm (String (_, _)) -> DB.type_string
| Imm (Block (_, _) | Symbol _ | Node (_, _))
- -> (error_tc ~loc:(lexp_location e) "Unsupported immediate value!";
+ -> ( if !Log.lsp_enabled then
+ error_tc ~loc:(lexp_location e) "Unsupported immediate value!";
DB.type_int)
| SortLevel SLz -> DB.type_level
| SortLevel (SLsucc e)
@@ -632,9 +638,10 @@ and check'' erased ctx e =
(* FIXME: Check recursive references. *)
| Var (((l, name), idx) as v)
-> if DB.set_mem idx erased then
- error_tc ~loc:l
- ("Var `" ^ maybename name ^ "`"
- ^ " can't be used here, because it's `erasable`");
+ ( if !Log.lsp_enabled then
+ error_tc ~loc:l
+ ("Var `" ^ maybename name ^ "`"
+ ^ " can't be used here, because it's `erasable`"));
lookup_type ctx v
| Susp (e, s) -> check erased ctx (push_susp e s)
| Let (l, defs, e)
@@ -665,15 +672,18 @@ and check'' erased ctx e =
match sort_compose ctx nctx l ak k1 k2 with
| SortResult k -> k
| SortInvalid
- -> error_tc ~loc:l "Invalid arrow: inner TypelLevel argument";
+ -> if !Log.lsp_enabled then
+ error_tc ~loc:l "Invalid arrow: inner TypelLevel argument";
mkSort (l, StypeOmega)
| SortK1NotType
- -> (error_tc ~loc:(lexp_location t1)
- "Not a proper type";
+ -> ( if !Log.lsp_enabled then
+ error_tc ~loc:(lexp_location t1)
+ "Not a proper type";
mkSort (l, StypeOmega))
| SortK2NotType
- -> (error_tc ~loc:(lexp_location t2)
- "Not a proper type";
+ -> ( if !Log.lsp_enabled then
+ error_tc ~loc:(lexp_location t2)
+ "Not a proper type";
mkSort (l, StypeOmega)))
| Lambda (ak, ((l,_) as v), t, e)
-> (let _k = check_type DB.set_empty ctx t in
@@ -690,12 +700,14 @@ and check'' erased ctx e =
match lexp'_whnf ft ctx with
| Arrow (ak', _v, t1, _l, t2)
-> if not (ak == ak') then
- (error_tc ~loc:(lexp_location arg)
+ ( if !Log.lsp_enabled 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)
+ | _ -> ( if !Log.lsp_enabled then
+ error_tc ~loc:(lexp_location arg)
("Calling a non function (type = "
^ lexp_string ft ^ ")!");
ft))
@@ -722,14 +734,15 @@ and check'' erased ctx e =
(* 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 _ ->
- DB.print_lexp_ctx ictx; print_newline ()
- )
- ("Field type "
- ^ lexp_string t
- ^ " is not a Type! ("
- ^ lexp_string lwhnf ^")");
+ | _tt -> if !Log.lsp_enabled then
+ (error_tc ~loc:(lexp_location t)
+ ~print_action:(fun _ ->
+ DB.print_lexp_ctx ictx; print_newline ()
+ )
+ ("Field type "
+ ^ lexp_string t
+ ^ " is not a Type! ("
+ ^ lexp_string lwhnf ^")"));
level),
DB.lctx_extend ictx v Variable t,
DB.set_sink 1 erased,
@@ -759,7 +772,8 @@ and check'' erased ctx e =
let ekind = get_type ctx etype in
let elvl = match lexp'_whnf ekind ctx with
| Sort (_, Stype l) -> l
- | _ -> Log.log_error ~loc:(lexp_location ekind)
+ | _ -> if !Log.lsp_enabled then
+ Log.log_error ~loc:(lexp_location ekind)
"Target lexp's kind is not a sort"; DB.level0 in
let it, aargs = call_split etype in
(match lexp'_whnf it ctx, aargs with
@@ -771,7 +785,8 @@ and check'' erased ctx e =
(* We don't check aarg's type, because we assume that `check`
* returns a valid type. *)
-> mksubst (S.cons aarg s) fargs aargs
- | _,_ -> (error_tc ~loc:l
+ | _,_ -> ( if !Log.lsp_enabled then
+ error_tc ~loc:l
"Wrong arg number to inductive type!"; s) in
let s = mksubst S.identity fargs aargs in
let ctx_extend_with_eq ctx subst hlxp nerased =
@@ -801,7 +816,8 @@ and check'' erased ctx e =
(ssink vdef s)
(mkCall (mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))]))
vdefs fieldtypes
- | _,_ -> (error_tc ~loc:l
+ | _,_ -> ( if !Log.lsp_enabled then
+ error_tc ~loc:l
"Wrong number of args to constructor!";
(erased, ctx, hlxp)) in
let hctor =
@@ -819,7 +835,9 @@ and check'' erased ctx e =
(match default with
| Some (v, d)
-> if diff <= 0 then
- warning_tc ~loc:l "Redundant default clause";
+ ( if !Log.lsp_enabled then
+ warning_tc ~loc:l "Redundant default clause"
+ else ());
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
@@ -830,9 +848,18 @@ and check'' erased ctx e =
(mkSusp ret (S.shift 2))
| None
-> if diff > 0 then
- error_tc ~loc:l ("Non-exhaustive match: "
- ^ string_of_int diff ^ " cases missing"))
- | _,_ -> error_tc ~loc:l "Case on a non-inductive type!");
+ (
+ if !Log.lsp_enabled then
+ (error_tc ~loc:l ("Non-exhaustive match: "
+ ^ string_of_int diff ^ " cases missing")
+ )
+ else ()
+ )
+ )
+ | _,_ -> if !Log.lsp_enabled then
+ error_tc ~loc:l "Case on a non-inductive type!"
+ else ()
+ );
ret
| Cons (t, (_l, name))
-> (match lexp'_whnf t ctx with
@@ -860,10 +887,12 @@ and check'' erased ctx e =
buildtype fargs) in
buildtype fargs
with Not_found
- -> (error_tc ~loc:l
+ -> ( if !Log.lsp_enabled then
+ error_tc ~loc:l
("Constructor \"" ^ name ^ "\" does not exist");
DB.type_int))
- | _ -> (error_tc ~loc:(lexp_location e)
+ | _ -> ( if !Log.lsp_enabled then
+ error_tc ~loc:(lexp_location e)
("Cons of a non-inductive type: "
^ lexp_string t);
DB.type_int))
=====================================
src/typer_lsp_server.ml
=====================================
@@ -39,8 +39,8 @@
open Log
open Util
-type state_after_processing = (log_entry list *
- ((vname * Lexp.lexp * Lexp.ltype) list list * Debruijn.elab_context)
+type state_after_processing = (log_entry list *
+ (((vname * Lexp.lexp * Lexp.ltype) list list * Debruijn.elab_context) option)
)
let log_entry_to_list (tab:log_entry list) : ((string * int * int * int * int) * log_level * string) list =
List.map (fun x -> let location = Option.get x.loc in
@@ -105,10 +105,18 @@ let readstring (str:string) =
Log.clear_log () ;
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)
+ let oast =
+ try
+ Some (Elab.lexp_decl_str str ectx)
+ with
+ | Log.Stop_Compilation msg
+ | Log.Internal_error msg
+ | Log.User_error msg -> None
+ in
+ (!Log.typer_log, oast)
let process_some_input_file (_file_contents : string) : state_after_processing =
+ Logs.err (fun k->k " %s" @@ "TEST TEST TEST");
readstring _file_contents
let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list =
@@ -131,30 +139,118 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list
diagnostic
) log_tab
- (*little method to test completion*)
- let little_fonc el =
- match el with
- | "lambda" -> "lambda (pattern) -> pattern ;"
- | "case" -> "case scrutinee \n | pattern -> pattern ;"
- | "let" -> "let_in_ (_=_ x ()) x ;"
- | "if" -> " if_then_else_ x \"x is true\" \"x is false\""
- | _ -> ""
-
- let little_kind el =
- match el with
- | "lambda" -> Lsp.Types.CompletionItemKind.Text
- | "case" -> Lsp.Types.CompletionItemKind.Function
- | "let" -> Lsp.Types.CompletionItemKind.Text
- | "if" -> Lsp.Types.CompletionItemKind.Text
- | _ -> Lsp.Types.CompletionItemKind.Text
-
- let little_detail el =
- match el with
- | "lambda" -> "define a function"
- | "case" -> "pattern matching"
- | "let" -> "let...in"
- | "if" -> "if...condition"
- | _ -> ""
+(*==============completion============================*)
+
+module Compl = struct
+
+ type k = Text | Method | Function | Constructor
+ | Field | Variable | Class | Interface
+ | Module | Property | Unit | Value
+ | Enum | Keyword | Snippet | Color
+ | File | Reference | Folder | EnumMember
+ | Constant | Struct | Event | Operator
+ | TypeParameter
+
+ type t = {
+ label:string;
+ newText:string;(*the text the completion will send*)
+ detail:string;
+ kind:k
+ }
+
+
+ let t_from_tuple (tup : (string * string * string * k) list) : t list =
+ List.map (fun x
+ -> let (label,newText,detail,kind) = x in
+ let ret = {
+ label = label ;
+ newText = newText ;
+ detail = detail ;
+ kind = kind
+ } in
+ ret
+ ) tup
+
+ let exemple_liste = [
+ ("lambda", "lambda (pattern) -> pattern ", "define a function", Text);
+ ("case", "case scrutinee \n | pattern -> pattern ", "pattern matching", Function);
+ ("let", "let_in_ (_=_ x ()) x ", "let...in", Text);
+ ("if", " if_then_else_ x \"x is true\" \"x is false\"", "if...condition", Text);
+ ("add", "add()", "add a element to a list", Method);
+ ]
+
+ let createKind (element:t) =
+ match element.kind with
+ | Text -> Lsp.Types.CompletionItemKind.Text
+ | Method -> Lsp.Types.CompletionItemKind.Method
+ | Function -> Lsp.Types.CompletionItemKind.Function
+ | Constructor -> Lsp.Types.CompletionItemKind.Constructor
+ | Field -> Lsp.Types.CompletionItemKind.Field
+ | Variable -> Lsp.Types.CompletionItemKind.Variable
+ | Class -> Lsp.Types.CompletionItemKind.Class
+ | Interface -> Lsp.Types.CompletionItemKind.Interface
+ | Module -> Lsp.Types.CompletionItemKind.Module
+ | Property -> Lsp.Types.CompletionItemKind.Property
+ | Unit -> Lsp.Types.CompletionItemKind.Unit
+ | Value -> Lsp.Types.CompletionItemKind.Value
+ | Enum -> Lsp.Types.CompletionItemKind.Enum
+ | Keyword -> Lsp.Types.CompletionItemKind.Keyword
+ | Snippet -> Lsp.Types.CompletionItemKind.Snippet
+ | Color -> Lsp.Types.CompletionItemKind.Color
+ | File -> Lsp.Types.CompletionItemKind.File
+ | Reference -> Lsp.Types.CompletionItemKind.Reference
+ | Folder -> Lsp.Types.CompletionItemKind.Folder
+ | EnumMember -> Lsp.Types.CompletionItemKind.EnumMember
+ | Constant -> Lsp.Types.CompletionItemKind.Constant
+ | Struct -> Lsp.Types.CompletionItemKind.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' |>
+ Base.List.mapi ~f:(fun line data ->
+ Base.String.split data ~on:' ' |>
+ Base.List.fold_map ~init:1 ~f:(fun pos word ->
+ let pos = pos + String.length word in
+ 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
+
+ let list_filter_by_character (liste: (string * int * int) list) (pos:int * int) : string =
+ let (word,_,_) =
+ List.find (fun (word,w_line,w_column) ->
+ let (cursor_line,cursor_column) = pos in
+ w_line == cursor_line && w_column == cursor_column
+ )
+ liste
+ in
+ word
+
+ let match_str (str:string) : Str.regexp =
+ str
+ |> Str.quote
+ |> Str.regexp
+
+
+ let complete (str:string) (liste: t list) =
+ match str with
+ | "List." -> List.filter (fun x ->
+ String.equal x.label "add"
+ )
+ liste
+ | str -> List.filter (fun x ->
+ let reg = match_str str in
+ Str.string_match reg x.label 0
+ )
+ liste
+
+ end
+
+(*==============completion============================*)
(*====================================Lexp parcourir===================================*)
@@ -264,8 +360,14 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list
| 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
+ let args_list = List.map
+ (fun (_ , e) -> browse_lexp ctx e cursor)
+ args
+ in
+
+ try
browse_list_lexp (fonc::args_list) cursor
+ with exe -> failwith "Exeption sur ce call !!!"
)
| Inductive (l, _label, args, cases)
@@ -282,7 +384,7 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list
((let lwhnf = Opslexp.lexp_whnf t ictx in
match Lexp.lexp_lexp' lwhnf with
| Sort (_, Stype _)
- when ak == Pexp.Aerasable (*&& impredicative_erase*)
+ when ak == Pexp.Aerasable
-> level
| Sort (_, Stype level')
-> Opslexp.mkSLlub ctx level
@@ -501,7 +603,7 @@ class lsp_server =
match Hashtbl.find buffers uri with
| state_after_processing -> let (_,ast) = state_after_processing in
- let (list_list, _) = ast in
+ let (list_list, _) = Option.get ast in
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 typer_loc = typer_pos_of_lsp_pos pos in
@@ -519,7 +621,7 @@ class lsp_server =
match Hashtbl.find buffers uri with
| state_after_processing -> let (_,ast) = state_after_processing in
- let (list_list, _) = ast in
+ let (list_list, _) = Option.get ast in
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 typer_loc = typer_pos_of_lsp_pos pos in
@@ -534,7 +636,7 @@ class lsp_server =
in
let e = Some r in
let f = Linol_lwt.return e in f
-
+
method! config_hover = Some (`Bool true)
method! config_definition = Some (`Bool true)
@@ -565,23 +667,26 @@ 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 (log_list,ast) = state_after_processing in
- let (list_list, ectx) = ast in*)
- let tab = ["lambda";"case";"let";"if"] in
+ | state_after_processing -> let trans_string = Compl.tranform_string doc_state.content in
+ let fbyline = Compl.list_filter_by_line trans_string (pos.line + 1) in
+ let word = Compl.list_filter_by_character fbyline ((pos.line + 1),pos.character) in
let typer_loc = typer_pos_of_lsp_pos pos in
let range = lsp_range_of_loc typer_loc in
- let r = List.map (fun x ->
- let label = x in
- let textEdit = `TextEdit (Lsp.Types.TextEdit.create ~range:range ~newText:(little_fonc x)) in
- let kind = little_kind x in
- let detail = little_detail x in
- let ci = Lsp.Types.CompletionItem.create
- ~label:label ~kind:kind
- ~textEdit:textEdit ~detail:detail ()
- in
- ci
-
- ) tab in
+
+ let tab_compl = Compl.complete word (Compl.t_from_tuple Compl.exemple_liste) in
+
+ let r = List.map (fun (x:Compl.t) ->
+ let label = x.label in
+ let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:(x.newText) in
+ let kind = Compl.createKind x in
+ let detail = x.detail in
+ let ci = Lsp.Types.CompletionItem.create
+ ~label:label ~kind:kind
+ ~textEdit:textEdit ~detail:detail ()
+ in
+ ci
+ ) tab_compl in
+
let e = Some (`List r) in
let f = Linol_lwt.return e in f
@@ -592,6 +697,7 @@ end
and runs it as a task. *)
let run () =
ignore (Arg.Set Log.lsp_enabled);
+ Logs.set_level ~all:true (Some Logs.Debug);
let s = new lsp_server in
let server = Linol_lwt.Jsonrpc2.create_stdio s in
let task = Linol_lwt.Jsonrpc2.run server in
=====================================
typer.ml
=====================================
@@ -30,9 +30,12 @@ let welcome_msg =
let arg_batch = ref false
-(*booléen utilisé pour démarrer le serveur.
- je l'ai mis true pour les tests
+(*
+booléen utilisé pour démarrer le serveur.
+mis true pour les tests
*)
+
+
let lsp_server = ref true
let arg_files = ref []
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/a1a11af523dcfe97f455c4ccc3736279…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/a1a11af523dcfe97f455c4ccc3736279…
You're receiving this email because of your account on gitlab.com.
1
0
09 Jui '21
Simon Génier deleted branch lexer-with-source at Stefan / Typer
--
You're receiving this email because of your account on gitlab.com.
1
0
[Git][monnier/typer][master] 2 commits: Rewrite the Lexer module in terms of source objects.
by Simon Génier (@ilovemonoids) 09 Jui '21
by Simon Génier (@ilovemonoids) 09 Jui '21
09 Jui '21
Simon Génier pushed to branch master at Stefan / Typer
Commits:
f289b62a by Simon Génier at 2021-05-29T12:12:42-04:00
Rewrite the Lexer module in terms of source objects.
This might not look useful, but it will simplify a great deal our next change of
add and end point to location records since all the location related code will
be in there source objects.
I ended up rewriting most of the Lexer. I tried to avoid doing that, but the
offset handling code was so mixed up with the rest than that turned out to give
worse code and a diff as unreadable. I'm pretty confident that that the changes
are OK since we are still able to load pervasives.typer and I wrote a few tests
for the trickier inner operators.
- - - - -
8d9a2367 by Simon Génier at 2021-06-09T12:28:31-04:00
Merge branch 'lexer-with-source'
- - - - -
3 changed files:
- src/lexer.ml
- src/option.ml
- src/source.ml
Changes:
=====================================
src/lexer.ml
=====================================
@@ -27,16 +27,6 @@ open Grammar
(*************** The Lexer phase *********************)
-let inc_cp (cp : charpos) (c : char) =
- (* Count char positions in utf-8: don't count the non-leading bytes. *)
- if utf8_head_p c then cp+1 else cp
-
-let digit_p char =
- let code = Char.code char
- in Char.code '0' <= code && code <= Char.code '9'
-
-type num_part = | NPint | NPfrac | NPexp
-
let unescape str =
let rec split b =
if b >= String.length str then []
@@ -45,108 +35,198 @@ let unescape str =
string_sub str b e :: split (e + 1)
in String.concat "" (split 0)
-let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos
- (* The returned Sexp may not be a Node. *)
- : sexp * pretoken list * bytepos * charpos =
- match pts with
- | [] -> (Log.internal_error "No next token!")
- | (Preblock (sl, bpts, el) :: pts) -> (Block (sl, bpts, el), pts, 0, 0)
- | (Prestring (loc, str) :: pts) -> (String (loc, str), pts, 0, 0)
- | (Pretoken ({file;line;column;docstr}, name) :: pts')
- -> let char = name.[bpos] in
- if digit_p char
- || (char = '-' (* FIXME: Handle '+' as well! *)
- && bpos + 1 < String.length name
- && digit_p (name.[bpos + 1])) then
- let rec lexnum bp cp (np : num_part) =
- if bp >= String.length name then
- ((if np == NPint then
- Integer ({file;line;column=column+cpos;docstr=docstr},
- Z.of_string (string_sub name bpos bp))
- else
- Float ({file;line;column=column+cpos;docstr=docstr},
- float_of_string (string_sub name bpos bp))),
- pts', 0, 0)
- else
- match name.[bp] with
- | ('0'|'1'|'2'|'3'|'4'|'5'|'6'|'7'|'8'|'9')
- -> lexnum (bp+1) (cp+1) np
- | '.' when np == NPint -> lexnum (bp+1) (cp+1) NPfrac
- | ('e'|'E') when not (np == NPexp) -> lexnum (bp+1) (cp+1) NPexp
- | ('+'|'-')
- when np == NPexp && (name.[bp-1] == 'e' || name.[bp-1] == 'E')
- -> lexnum (bp+1) (cp+1) NPexp
- | _
- -> ((if np == NPint then
- Integer ({file;line;column=column+cpos;docstr=docstr},
- Z.of_string (string_sub name bpos bp))
- else
- Float ({file;line;column=column+cpos;docstr=docstr},
- float_of_string (string_sub name bpos bp))),
- pts, bp, cp)
- in lexnum (bpos+1) (cpos+1) NPint
- else if bpos + 1 >= String.length name then
- (hSymbol ({file;line;column=column+cpos;docstr=docstr},
- string_sub name bpos (String.length name)),
- pts', 0, 0)
- else if stt.(Char.code name.[bpos]) = CKseparate then
- (hSymbol ({file;line;column=column+cpos;docstr=docstr},
- string_sub name bpos (bpos + 1)),
- pts, bpos+1, cpos+1)
- else
- let rec lexsym bpos cpos =
- let mksym epos escaped
- = if epos = bpos then epsilon {file;line;column=column+cpos;docstr=docstr} else
- let rawstr = string_sub name bpos epos in
- let str = if escaped then unescape rawstr else rawstr in
- hSymbol ({file;line;column=column+cpos;docstr=docstr}, str) in
- let rec lexsym' prec lf bp cp escaped =
- if bp >= String.length name then
- (lf (mksym (String.length name) escaped), pts', 0, 0)
- else
- let char = name.[bp] in
- let bp' = bp + 1 in
- let is_last = bp' >= String.length name in
- match stt.(Char.code char) with
- | _ when char == '\\' && not is_last
- (* Skip next char, in case it's a special token. *)
- (* For utf-8, this cp+2 is risky but actually works: \ counts
- * as 1 and if the input is valid utf-8 the next byte has to
- * be a leading byte, so it has to count as 1 as well ;-) *)
- -> lexsym' prec lf (bp+2) (cp+2) true
- | CKseparate -> (lf (mksym bp escaped), pts, bp, cp)
- (* Turn `inner` infix operators, such as the "." of
- * "Module.elem" into the equivalent of (__.__ Module elem). *)
- | CKinner prec'
- (* To be considered `inner`, an operator char needs to have
- * something on its LHS or its RHS, otherwise, treat it as
- * a normal char, `.` can be a normal operator as well. *)
- when bpos != bp
- || (not is_last
- && CKseparate != (stt.(Char.code name.[bp'])))
- || not (lf dummy_epsilon = dummy_epsilon)
- -> let left = mksym bp escaped in
- let op = hSymbol ({file;line;column=column+cp;docstr=docstr},
- "__" ^ String.sub name bp 1 ^ "__") in
- let bpos = bp' in
- let cpos = inc_cp cp char in
- let lf' = if prec' > prec then
- (fun s -> lf (Node (op, [left; s])))
- else
- (fun s -> Node (op, [lf left; s])) in
- lexsym bpos cpos prec' lf'
- bpos cpos false
- | _ -> lexsym' prec lf (bp+1) (inc_cp cp char) escaped
- in lexsym'
- in lexsym bpos cpos 0 (fun s -> s) bpos cpos false
-
-let lex tenv (pts : pretoken list) : sexp list =
- let rec gettokens pts bpos cpos acc =
- match pts with
+let lex_number
+ (source : #Source.t)
+ (start_location : Source.Location.t)
+ (start_offset : int)
+ : sexp =
+
+ let rec lex_exponent () =
+ match source#peek_char with
+ | Some ('0' .. '9')
+ -> source#advance;
+ lex_exponent ()
+
+ | _
+ -> let source = source#slice_from_offset start_offset in
+ Float (start_location, float_of_string source)
+ in
+
+ let lex_exponent_sign () =
+ match source#peek_char with
+ | Some ('0' .. '9' | '+' | '-')
+ -> source#advance;
+ lex_exponent ()
+
+ (* TODO: error if there are no signs or digits after the 'e'? *)
+ | _
+ -> let source = source#slice_from_offset start_offset in
+ Float (start_location, float_of_string source)
+ in
+
+ let rec lex_fractional () =
+ match source#peek_char with
+ | Some ('0' .. '9')
+ -> source#advance;
+ lex_fractional ()
+
+ | Some ('e' | 'E')
+ -> source#advance;
+ lex_exponent_sign ()
+
+ | _
+ -> let source = source#slice_from_offset start_offset in
+ Float (start_location, float_of_string source)
+ in
+
+ let rec lex_integer () =
+ match source#peek_char with
+ | Some ('0' .. '9')
+ -> source#advance;
+ lex_integer ()
+
+ | Some ('.')
+ -> source#advance;
+ lex_fractional ()
+
+ | Some ('e' | 'E')
+ -> source#advance;
+ lex_exponent_sign ()
+
+ | _
+ -> let source = source#slice_from_offset start_offset in
+ Integer (start_location, Z.of_string source)
+ in
+
+ lex_integer ()
+
+(* Splits one symbol from the beginning of the source. *)
+let lex_symbol
+ (token_env : token_env)
+ (source : #Source.t)
+ (doc : string)
+ (start_location : Source.Location.t)
+ (start_offset : int)
+ : sexp =
+
+ let mksym start_location start_offset escaped =
+ if Int.equal start_offset source#current_offset
+ then epsilon start_location
+ else
+ let raw_name = source#slice_from_offset start_offset in
+ let name = if escaped then unescape raw_name else raw_name in
+ hSymbol (start_location, name)
+ in
+
+ let rec loop start_location start_offset prec lf (escaped : bool) =
+ match source#peek_char with
+ | None
+ -> lf (mksym start_location start_offset escaped)
+
+ | Some c
+ -> (match token_env.(Char.code c) with
+ | CKseparate
+ -> lf (mksym start_location start_offset escaped)
+
+ | CKinner prec'
+ -> let left = mksym start_location start_offset escaped in
+ let op_location = source#current_location doc in
+
+ (* To be considered `inner`, an operator char needs to have
+ something on its LHS or its RHS, otherwise, treat it as a
+ normal char. `.` can be the normal function composition
+ operator as well. *)
+ let lhs_p = start_offset != source#current_offset in
+ source#advance;
+ let rhs_p =
+ (match source#peek_char with
+ | None -> false
+ | Some c' -> CKseparate != token_env.(Char.code c'))
+ in
+ if lhs_p || rhs_p || lf dummy_epsilon <> dummy_epsilon
+ then
+ let op = hSymbol (op_location, Printf.sprintf "__%c__" c) in
+ let lf' =
+ if prec' > prec
+ then fun s -> lf (Node (op, [left; s]))
+ else fun s -> Node (op, [lf left; s])
+ in
+ loop (source#current_location doc) source#current_offset prec' lf' false
+ else
+ loop start_location start_offset prec lf escaped
+
+ | CKnormal
+ -> (source#advance;
+ let is_last = Option.is_none source#peek_char in
+ match c with
+ (* Skip next char, in case it's a special token. For utf-8,
+ simply advancing is risky but actually works: '\' counts as 1
+ and if the input is valid utf-8 the next byte has to be a
+ leading byte, so it has to count as 1 as well ;-) *)
+ | '\\' when not is_last
+ -> source#advance;
+ loop start_location start_offset prec lf true
+
+ | _ -> loop start_location start_offset prec lf escaped))
+ in
+ loop start_location start_offset 0 (fun s -> s) false
+
+let split_presymbol
+ (token_env : token_env)
+ (source : #Source.t)
+ (doc : string)
+ : sexp list =
+
+ let rec loop (acc : sexp list) : sexp list =
+ match source#peek_char with
+ | None -> List.rev acc
+ | Some (c)
+ -> let start_offset = source#current_offset in
+ let start_location = source#current_location doc in
+ let token =
+ match c with
+ (* A negative number literal, or a symbol starting with '-'. *)
+ | '-'
+ -> (source#advance;
+ match source#peek_char with
+ | Some ('0' .. '9')
+ -> lex_number source start_location start_offset
+ | _
+ -> lex_symbol token_env source doc start_location start_offset)
+
+ | '0' .. '9'
+ -> (source#advance;
+ lex_number source start_location start_offset)
+
+ | _ when token_env.(Char.code c) = CKseparate
+ -> source#advance;
+ let name = source#slice_from_offset start_offset in
+ hSymbol (start_location, name)
+
+ | _
+ -> lex_symbol token_env source doc start_location start_offset
+ in
+ loop (token :: acc)
+ in
+ loop []
+
+let lex (token_env : token_env) (pretokens : pretoken list) : sexp list =
+ let rec loop pretokens acc =
+ match pretokens with
| [] -> List.rev acc
- | _ -> let (tok, pts, bpos, cpos) = nexttoken tenv pts bpos cpos
- in gettokens pts bpos cpos (tok :: acc) in
- gettokens pts 0 0 []
+
+ | Preblock (start_location, block_pretokens, end_location) :: pretokens'
+ -> loop pretokens' (Block (start_location, block_pretokens, end_location) :: acc)
+
+ | Prestring (location, text) :: pretokens'
+ -> loop pretokens' (String (location, text) :: acc)
+
+ | Pretoken ({file; line; column; docstr}, name) :: pretokens'
+ -> let source = new Source.source_string ~file ~line ~column name in
+ let tokens = split_presymbol token_env source docstr in
+ loop pretokens' (List.rev_append tokens acc)
+ in
+ loop pretokens []
let lex_source (source : #Source.t) tenv =
let pretoks = prelex source in
@@ -155,4 +235,3 @@ let lex_source (source : #Source.t) tenv =
let sexp_parse_source (source : #Source.t) tenv grm limit =
let toks = lex_source source tenv in
sexp_parse_all_to_list grm toks limit
-
=====================================
src/option.ml
=====================================
@@ -40,3 +40,8 @@ let is_some (o : 'a option) : bool =
match o with
| Some _ -> true
| None -> false
+
+let is_none (o : 'a option) : bool =
+ match o with
+ | Some _ -> false
+ | None -> true
=====================================
src/source.ml
=====================================
@@ -131,13 +131,13 @@ class source_file file_name = object (self)
end
class source_string
- ?(base_line : int = first_line_of_file)
- ?(base_column : int = first_column_of_line)
- ?(file_name : string = "<string>")
+ ?(file : string = "<string>")
+ ?(line : int = first_line_of_file)
+ ?(column : int = first_column_of_line)
source
=
object
- inherit t base_line base_column file_name
+ inherit t line column file
val mutable offset = 0
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/b8d1df5b6886203e354594b2096aec7b…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/b8d1df5b6886203e354594b2096aec7b…
You're receiving this email because of your account on gitlab.com.
1
0
[Git][monnier/typer] Deleted branch type-macro-improvements
by Jean-Alexandre Barszcz (@jabarszcz) 07 Jui '21
by Jean-Alexandre Barszcz (@jabarszcz) 07 Jui '21
07 Jui '21
Jean-Alexandre Barszcz deleted branch type-macro-improvements at Stefan / Typer
--
You're receiving this email because of your account on gitlab.com.
1
0
[Git][monnier/typer][master] 3 commits: Fix nix shell and dune details
by Jean-Alexandre Barszcz (@jabarszcz) 07 Jui '21
by Jean-Alexandre Barszcz (@jabarszcz) 07 Jui '21
07 Jui '21
Jean-Alexandre Barszcz pushed to branch master at Stefan / Typer
Commits:
8e1be507 by Jean-Alexandre Barszcz at 2021-05-31T16:39:39-04:00
Fix nix shell and dune details
- - - - -
dc07e915 by Jean-Alexandre Barszcz at 2021-05-31T16:39:39-04:00
* btl/pervasive.typer (type-impl): Accept implicit type params.
Also, allow type definitions at other type levels than 0, with an
annotation.
- - - - -
b8d1df5b by Jean-Alexandre Barszcz at 2021-05-31T16:39:39-04:00
* btl/pervasive.typer (type-impl): Keep the constructors in order.
- - - - -
5 changed files:
- GNUmakefile
- README.md
- btl/pervasive.typer
- shell.nix
- tests/elab_test.ml
Changes:
=====================================
GNUmakefile
=====================================
@@ -9,7 +9,7 @@ DEPSORT_FILES := $(shell ocamldep -sort -I src $(SRC_NO_DEBUG))
DUNE_PROFILE = dev
# DUNE_PROFILE = release
-# Set COMPILE_MODE to native to build ocaml code with ocamlopt.
+# Set COMPILE_MODE to `exe` for native builds.
COMPILE_MODE ?= bc
# DEBUG ?= 1
@@ -28,7 +28,7 @@ debug: debug_util.$(COMPILE_MODE)
# interactive typer
typer.$(COMPILE_MODE):
- $(DUNE) --profile $(DUNE_PROFILE) build ./typer.$(COMPILE_MODE)
+ $(DUNE) build ./typer.$(COMPILE_MODE) --profile $(DUNE_PROFILE)
debug_util.$(COMPILE_MODE):
$(DUNE) build ./debug_util.$(COMPILE_MODE)
@@ -37,7 +37,7 @@ debug_util.$(COMPILE_MODE):
# be confusing if you don't know Dune, so we pass the --force flag to rerun all
# the tests no matter what.
tests:
- $(DUNE) --force test
+ $(DUNE) test --force
# There is nothing here. I use this to test if opam integration works
install: tests
=====================================
README.md
=====================================
@@ -17,7 +17,7 @@ Status []
By default, Dune creates a '_build' folder which holds all the compiled files.
* `make typer`: build Typer interpreter (`./typer_cli.bc`).
-* `COMPILE_MODE=native make typer`: build Typer interpreter (`./typer_cli.exe`).
+* `COMPILE_MODE=exe make typer`: build Typer interpreter (`./typer_cli.exe`).
* `make debug`: build typer with debug info (`./debug_util.bc`).
* `make tests`: run interpreter's tests.
=====================================
btl/pervasive.typer
=====================================
@@ -308,17 +308,34 @@ type-impl = lambda (x : List Sexp) ->
(lambda _ -> (nil : List Sexp)) % Float
(lambda _ -> (nil : List Sexp)); % List of Sexp
- get-type : Sexp -> Sexp;
- get-type sxp =
- Sexp_dispatch sxp
- (lambda s ss -> case (Sexp_eq s (Sexp_symbol "_:_"))
- | true => List_nth 1 ss Sexp_error
- | false => sxp)
- (lambda _ -> sxp)
- (lambda _ -> Sexp_error)
- (lambda _ -> Sexp_error)
- (lambda _ -> Sexp_error)
- (lambda _ -> Sexp_error);
+ %% Takes an arrow type and a parameter (possibly named using
+ %% `:`/`::`/`:::`), and prepends the corresponding arrow
+ %% (`->`/`=>`/`≡>`) to the arrow type given as argument.
+ add-arg-arrow : Sexp -> Sexp -> Sexp;
+ add-arg-arrow arrow-type arg =
+ let default_arr =
+ Sexp_node (Sexp_symbol "_->_") (cons arg (cons arrow-type nil)) in
+ Sexp_dispatch arg
+ (lambda s ss ->
+ let single-colon-arg =
+ (Sexp_node (Sexp_symbol "_:_")
+ (cons (List_head Sexp_error ss)
+ (cons (List_nth 1 ss Sexp_error) nil)));
+ arrow-args = (cons single-colon-arg (cons arrow-type nil)) in
+ case (Sexp_eq s (Sexp_symbol "_:_"))
+ | true => Sexp_node (Sexp_symbol "_->_") arrow-args
+ | false =>
+ (case (Sexp_eq s (Sexp_symbol "_::_"))
+ | true => Sexp_node (Sexp_symbol "_=>_") arrow-args
+ | false =>
+ (case (Sexp_eq s (Sexp_symbol "_:::_"))
+ | true => Sexp_node (Sexp_symbol "_≡>_") arrow-args
+ | false => default_arr)))
+ (lambda _ -> default_arr)
+ (lambda _ -> Sexp_error)
+ (lambda _ -> Sexp_error)
+ (lambda _ -> Sexp_error)
+ (lambda _ -> Sexp_error);
get-head = List_head Sexp_error;
@@ -328,24 +345,30 @@ type-impl = lambda (x : List Sexp) ->
%% Expression is Sexp_node (Sexp_symbol "|") (list)
%% we only care about the list bit
lst = get-list expr;
-
- %% head is (Sexp_node type-name (arg list))
- name = get-head lst;
ctor = List_tail lst;
- type-name = get-name name;
+ %% head+ is (Sexp_node type-name (arg list)), optionally wrapped
+ %% with a type annotation (<head> : Type_ l)
+ head+ = get-head lst;
+
+ %% head-pair is a 2-list, which adds a default type annotation to head+
+ head-pair = case Sexp_eq (get-name head+) (Sexp_symbol "_:_")
+ | true => get-list head+
+ | false => cons head+ (cons (Sexp_symbol "Type") nil);
+
+ head = List_nth 0 head-pair Sexp_error;
+ type-type = List_nth 1 head-pair Sexp_error;
+ type-name = get-name head;
+ type-args = get-list head;
%% Create the inductive type definition.
inductive = Sexp_node (Sexp_symbol "typecons")
- (cons name ctor);
+ (cons head ctor);
%% Declare the inductive type as a function
%% Useful for recursive type
- type-decl = quote ((uquote (get-name name)) : (uquote (
- (List_foldl (lambda args arg ->
- Sexp_node (Sexp_symbol "_->_") (cons (get-type arg) (cons args nil)))
- %% FIXME: Don't hardcode TypeLevel.z!
- (Sexp_symbol "Type") (List_reverse (get-args name) nil))
+ type-decl = quote ((uquote type-name) : (uquote (
+ (List_foldl add-arg-arrow type-type (List_reverse type-args nil))
)));
decl = make-decl type-name inductive;
@@ -354,9 +377,8 @@ type-impl = lambda (x : List Sexp) ->
ctors = let for-each : List Sexp -> Sexp -> Sexp;
for-each ctr acc = case ctr
| cons hd tl =>
- let acc2 = chain-decl (make-cons (get-name hd)
- type-name)
- acc
+ let acc2 = chain-decl acc (make-cons (get-name hd)
+ type-name)
in for-each tl acc2
| nil => acc
in for-each ctor (Sexp_node (Sexp_symbol "_;_") nil)
=====================================
shell.nix
=====================================
@@ -3,7 +3,7 @@ pkgs.mkShell {
name = "typer";
buildInputs =
with pkgs.ocamlPackages; [
- pkgs.gnumake ocaml ocamlbuild findlib utop # tooling
+ pkgs.gnumake ocaml dune_2 findlib utop # tooling
zarith # ocaml libraries
merlin # for emacs
];
=====================================
tests/elab_test.ml
=====================================
@@ -217,4 +217,18 @@ test =
(getProof (decideBoolEq : Decidable (Eq true true)) : Eq true true);
|}
+let _ = add_elab_test_decl
+ "Implicit type parameters"
+ {|
+type Not (ℓ ::: TypeLevel) (prop : Type_ ℓ) : Type_ ℓ
+ | mkNot ((contra : prop) -> False);
+
+type Decidable (ℓ ::: TypeLevel) (prop : Type_ ℓ) : Type_ ℓ
+ | yes (p ::: prop)
+ | no (p ::: Not prop);
+
+type Lift (l ::: TypeLevel) (t :: Type_ l) (x : t)
+ | mkLift;
+ |}
+
let _ = run_all ()
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/c5ef2f59f36e51ab6c709193a01bb355…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/c5ef2f59f36e51ab6c709193a01bb355…
You're receiving this email because of your account on gitlab.com.
1
0
[Git][monnier/typer] Pushed new branch instance-args
by Jean-Alexandre Barszcz (@jabarszcz) 01 Jui '21
by Jean-Alexandre Barszcz (@jabarszcz) 01 Jui '21
01 Jui '21
Jean-Alexandre Barszcz pushed new branch instance-args at Stefan / Typer
--
View it on GitLab: https://gitlab.com/monnier/typer/-/tree/instance-args
You're receiving this email because of your account on gitlab.com.
1
0