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/fd27756b4e6d5c378c070ef5a206a4acb...