Soilihi BEN SOILIHI BOINA pushed to branch add-proj at Stefan / Typer

Commits: 0b2b72bb by Soilih at 2022-02-05T00:31:01-05:00 -

- - - - -

8 changed files:

- − .vscode/launch.json - btl/pervasive.typer - src/elab.ml - src/elexp.ml - src/eval.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml

Changes:

===================================== .vscode/launch.json deleted ===================================== @@ -1,15 +0,0 @@ -{ - // Use IntelliSense to learn about possible attributes. - // Hover to view descriptions of existing attributes. - // For more information, visit: https://go.microsoft.com/fwlink/?linkid=830387 - "version": "0.2.0", - "configurations": [ - { - "type": "pwa-chrome", - "request": "launch", - "name": "Launch Chrome against localhost", - "url": "http://localhost:8080", - "webRoot": "${workspaceFolder}" - } - ] -} \ No newline at end of file

===================================== btl/pervasive.typer ===================================== @@ -424,7 +424,7 @@ BoolMod = (##datacons (_ := Bool) (_ := true) (_ := false);

Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b)); -pair = datacons Pair pair; +pair = datacons Pair pair;

%% Triplet (tuple with 3 values) type Triplet (a : Type) (b : Type) (c : Type)

===================================== src/elab.ml ===================================== @@ -1731,9 +1731,12 @@ let sform_proj ctx loc sargs _ = match sargs with | [lxp;(Symbol (loca,str))] -> let (ret,_) = infer lxp ctx in - let e = mkProj (loc,ret,(loca,str)) in + let e = mkProj (loc,ret,(loca,str)) in (e, Lazy) - | _ -> sexp_error loc "Unrecognized proj expression"; + | [_;_] + -> sexp_error loc "Second argument is not a Symbol!"; + sform_dummy_ret ctx loc + | _ -> sexp_error loc "Wrong arg number!"; sform_dummy_ret ctx loc

let rec infer_level ctx se : lexp =

===================================== src/elexp.ml ===================================== @@ -141,7 +141,7 @@ and elexp_string lxp = | Builtin((_, s)) -> s | Var((_, s), i) -> L.maybename s ^ "[" ^ string_of_int i ^ "]" | Proj (_,lxp,i) - -> "( _._ " ^ elexp_string lxp ^ " " ^ (string_of_int 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 ===================================== @@ -464,16 +464,11 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) (List.map (fun e -> eval e ctx trace) args) (* Proj *) | Proj (loc, e, i) - -> let vt = eval' e ctx in - ( - match vt with - | Vcons (_, vtl) -> List.nth vtl i - | _ -> error - loc - "Connot find a value in position %d \n" i - ) - - + -> (match eval' e ctx with + | Vcons (_, vtl) -> List.nth vtl i + | _ -> error + loc + "Proj on a non-datatype constructor: %s \n" (elexp_string e)) (* Case *) | Case (loc, target, pat, dflt) -> (eval_case ctx trace loc target pat dflt)

===================================== src/lexp.ml ===================================== @@ -248,7 +248,7 @@ let lexp'_hash (lp : lexp') = -> 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))) + (U.combine_hash (Hashtbl.hash lxp) (Hashtbl.hash lbl)))

(* Equality function for hash table * using physical equality for "sub-lexp" and compare for `subst`. *) @@ -661,7 +661,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) + | 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 @@ -985,8 +985,8 @@ and lexp_str ctx (exp : lexp) : string =

| Var ((_loc, name), idx) -> maybename name ^ (index idx) ;

- | Proj (_,lxp,(_,str)) - -> "( _._ " ^ lexp_str' lxp ^ " " ^ str ^ " )" + | Proj (_, lxp, (_, str)) + -> "( __.__ " ^ lexp_str' lxp ^ " " ^ str ^ " )"

| Metavar (idx, subst, (_loc, name)) (* print metavar result if any *)

===================================== src/opslexp.ml ===================================== @@ -773,7 +773,7 @@ and check'' erased ctx e = (* We found our field! *) -> if not (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 erasable field: %s" label; Lexp.impossible) | (_, vdef, _)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with @@ -965,7 +965,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 (_,lxp,_) -> fv lxp + | Proj (_, lxp, _) -> fv lxp | Susp (e, s) -> fv (push_susp e s) | Let (_, defs, e) -> let len = List.length defs in @@ -1082,7 +1082,7 @@ and get_type ctx e = (* We found our field! *) -> if not (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 erasable field: %s" label; Lexp.impossible) | (_, vdef, _)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with @@ -1231,22 +1231,19 @@ let pos_of_label lctx label e : int = match lexp'_whnf it lctx, aargs with | Inductive (_, _, _, constructors), _ when SMap.cardinal constructors = 1 - -> + -> let (_, st) = label in (match SMap.bindings constructors with - | [(_,l)] -> let rec foo label (l : (arg_kind * vname * ltype) list) (c: int) : int= + | [(_,l)] -> let rec find_index label (l : (arg_kind * vname * ltype) list) (c: int) : int = match l with | [] -> let (loc,st) = label in - Log.log_error ~loc:loc "Label: %s Not Found!" st; 0 - | hd::tl -> match hd with - | (_, (_, Some vn), _ ) - -> let (_,st) = label in - if (String.equal vn st) then c - else foo label tl (c + 1) - | _ -> foo label tl (c + 1) + Log.log_error ~loc:loc "Label Not Found: %s" st; 0 + | (_, (_, Some vn), _ )::_ when (String.equal vn st) + -> c + | _::tl -> find_index label tl (c + 1) in - foo label l 0 - | _ -> let (loc,_) = label in + find_index label l 0 + | _ -> let (loc, _) = label in Log.log_fatal ~loc:loc "Wrong arg number to inductive type!" ) | Inductive _, _

===================================== src/unification.ml ===================================== @@ -69,7 +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 + | 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/-/commit/0b2b72bb4d02232c2f58caef2e82b15557...