Stefan pushed to branch unification at Stefan / Typer
Commits: 49dad956 by Pierre Delaunay at 2016-09-07T15:13:34-04:00 finished type_ macro
Changes to be committed: * samples/inductive.typer - finished the type_ macro * samples/int_index_inconsistency.typer - type index are inconsistent * src/builtin.ml - improved error message
- - - - - 3ef3619c by Pierre Delaunay at 2016-09-07T15:15:21-04:00 Merge branch 'master' of gitlab.com:monnier/typer
- - - - - bae92e62 by Pierre Delaunay at 2016-09-08T09:50:00-04:00 updated the type_ macro. - Formal args were not processed correctly. - Added new examples - Modfied style
Changes to be committed: * samples/inductive.typer
- - - - - 713bde4f by Pierre Delaunay at 2016-09-11T09:58:49-04:00 Macro are now expanded by a builtin function.
Changes to be committed: * btl/types.typer: added `expand_macro_` builtin * src/builtin.ml: added `expand_macro_` as a predef * src/eval.ml: `expand_macro_` is a builtin function * src/lparse.ml: - updated `handle_macro_call` to call `expand_macro_` instead of expanding the macro by itself
- - - - - 0ae8be8b by Pierre Delaunay at 2016-09-12T20:55:36-04:00 Changes to be committed: * src/lparse.ml: Fix `case` handling
`case` now looks up the pattern type and add them to the environement. Which allows us to write things like:
`case m | Macro_ f => f args;`
(before a dummy type was added, thus an error occured because f was not considered a function)
* src/util.ml: improved `print_trace` behavior print the last 50 call recorded instead of the first 50
* btl/types.typer * src/eval.ml - expand_macro is now defined in typer
- - - - - 010aa5dc by Pierre Delaunay at 2016-09-12T21:15:58-04:00 Remove dead code, and silence some warnings
Changes to be committed: * btl/types.typer * src/eval.ml * src/lparse.ml
- - - - - d5d7b301 by Pierre Delaunay at 2016-09-13T01:06:15-04:00 new function `lexp_to_pexp`
- - - - - ad319791 by Stefan Monnier at 2016-09-14T14:49:44-04:00 Type check values added via env_extend
* src/debruijn.ml (elab_context): New name. (ectx_to_lctx): New function. (ectx_extend_rec): New function. (env_extend): Use 0 as db_offset since these are non-recursive.
* src/lparse.ml (_shift_glob): Remove. (senv_lookup): Don't redefine. (ctx_define): New function. (lexp_call): Update to new arg type of lexp_whnf. (lexp_read_pattern): Use ctx_define. (_lexp_rec_decl.tctx): Rename `expr` -> `decl` since it's a declaration. (default_lctx): Use ctx_define.
* src/opslexp.ml (lookup_type, lookup_value): Move earlier. (conv_p'): Use structural equality for sorts. (lexp_whnf): Don't use elab_context since this is also used elsewhere.
- - - - - 5faabc18 by Stefan Monnier at 2016-09-14T15:09:19-04:00 Merge branch 'trunk' into unification
- - - - -
13 changed files:
- + +tmp - btl/types.typer - samples/inductive.typer - + samples/int_index_inconsistency.typer - src/builtin.ml - src/debruijn.ml - src/eval.ml - src/fmt.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml - src/util.ml - tests/eval_test.ml
Changes:
===================================== +tmp ===================================== --- /dev/null +++ b/+tmp @@ -0,0 +1 @@ +Subproject commit e54bbd6d3f50ce539b9669e07cec546057c0381d
===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -107,6 +107,10 @@ float_ = Built-in "float_" (Float -> Sexp); Macro = inductive_ (dMacro) (Macro_ (List Sexp -> Sexp)); Macro_ = inductive-cons Macro Macro_ ;
+expand_macro_ : Macro -> List Sexp -> Sexp; +expand_macro_ m args = case m + | Macro_ f => (f args); + sexp_dispatch_ = Built-in "sexp_dispatch_" ( (a : Type) ≡> Sexp
===================================== samples/inductive.typer ===================================== --- a/samples/inductive.typer +++ b/samples/inductive.typer @@ -1,46 +1,122 @@ +% build a declaration +% var-name = value-expr; +make-decl : Sexp -> Sexp -> Sexp; +make-decl var-name value-expr = + node_ (symbol_ "_=_") + (cons (a := Sexp) var-name + (cons (a := Sexp) value-expr (nil (a := Sexp)))); + +% build inductive-cons +% ctor-name = inductive-cons type-name ctor-name; +make-cons : Sexp -> Sexp -> Sexp; +make-cons ctor-name type-name = + make-decl ctor-name + (node_ (symbol_ "inductive-cons") + (cons (a := Sexp) type-name + (cons (a := Sexp) ctor-name (nil (a := Sexp))))); + +% buil type annotation +% var-name : type-expr; +make-ann : Sexp -> Sexp -> Sexp; +make-ann var-name type-expr = + node_ (symbol_ "_:_") + (cons (a := Sexp) var-name + (cons (a := Sexp) type-expr (nil (a := Sexp)))); + + type-impl = lambda (x : List Sexp) -> % x follow the mask -> (_|_ Nat zero (succ Nat)) % Type name --^ ^------^ constructors
+ let sexp_nil = (nil (a := Sexp)) in + + % Return a list contained inside a node sexp + let get-list : Sexp -> List Sexp; + get-list node = sexp_dispatch_ (a := List Sexp) node + (lambda op lst -> lst) % Nodes + (lambda _ -> sexp_nil) % Symbol + (lambda _ -> sexp_nil) % String + (lambda _ -> sexp_nil) % Integer + (lambda _ -> sexp_nil) % Float + (lambda _ -> sexp_nil) in % List of Sexp + + % Get a name from a sexp + % - (name t) -> name + % - name -> name + let get-name : Sexp -> Sexp; + get-name sxp = + sexp_dispatch_ (a := Sexp) sxp + (lambda op lst -> get-name op) % Nodes + (lambda str -> symbol_ str) % Symbol + (lambda _ -> symbol_ "error") % String + (lambda _ -> symbol_ "error") % Integer + (lambda _ -> symbol_ "error") % Float + (lambda _ -> symbol_ "error") in % List of Sexp + % Get expression let expr = head (a := Sexp) x in - let sexp_nil = nil (a := Sexp) in
% Expression is node_ (symbol_ "|") (list) % we only care about the list bit - - let get-list = (lambda (node : Sexp) -> - sexp_dispatch_ (a := List Sexp) node - (lambda (op : Sexp) -> (lambda (lst : List Sexp) -> lst)) % Nodes - (lambda (str : String) -> sexp_nil) % Symbol - (lambda (str : String) -> sexp_nil) % String - (lambda (int : Int) -> sexp_nil) % Integer - (lambda (float : Float) -> sexp_nil) % Float - (lambda (lst : List Sexp) -> sexp_nil)) in % List of Sexp - let lst = get-list expr in
- let name = head (a := Sexp) lst in - let ctor = tail (a := Sexp) lst in + % head is (node_ type-name (arg list)) + let name = head (a := Sexp) lst; + ctor = tail (a := Sexp) lst in
- % Create a forward declaration in case the declaration is recursive - let fdecl = node_ (symbol_ "_:_") - (cons (a := Sexp) name - (cons (a := Sexp) (symbol_ "Type") sexp_nil)) in + let type-name = get-name name in
% Create the inductive type definition let inductive = node_ (symbol_ "inductive_") - (cons (a := Sexp) (symbol_ "dlabel") ctor) in + (cons (a := Sexp) name ctor) in
- let decl = node_ (symbol_ "_=_") - (cons (a := Sexp) name - (cons (a := Sexp) inductive sexp_nil)) in + % Create a forward declaration in case the declaration is recursive + % let fdecl = make-ann type-name (symbol_ "Type") in + let decl = make-decl type-name inductive in + + % Add constructors + let ctors = + let for-each : List Sexp -> List Sexp -> List Sexp; + for-each ctr acc = case ctr + | cons hd tl => ( + let acc2 = cons (a := Sexp) (make-cons (get-name hd) type-name) acc in + for-each tl acc2) + | nil => acc + in for-each ctor (nil (a := Sexp)) in + + % return decls + % cons (a := Sexp) fdecl % Forward declaration + (cons (a := Sexp) decl % inductive type declaration + ctors); % constructor declarations
- cons (a := Sexp) fdecl - (cons (a := Sexp) decl sexp_nil);
type_ = Macro_ type-impl;
-type Nat - | zero - | succ Nat; +% (type_ (_|_ (Either t1 t2) (either-first t1) (either-second t2))) +type Either t1 t2 + | either-first t1 + | either-second t2; + +type Pair t1 t2 + | pair t1 t2; + +type Point t + | point (x : t) (y : t); + +get-first : (a : Type) => (b : Type) => Pair -> a; +get-second : (a : Type) => (b : Type) => Pair -> b; + +get-first p = case p | pair a b => a; +get-second p = case p | pair a b => b; + +get-x : (a : Type) => Point -> a; +get-y : (a : Type) => Point -> a; +get-x p = case p | point x y => x; +get-y p = case p | point x y => y; + + +% transformed to: +% Nat : Type; +% Nat = inductive_ (Nat) (succ Nat) (zero); +% zero = inductive-cons Nat zero; +% succ = inductive-cons Nat succ; \ No newline at end of file
===================================== samples/int_index_inconsistency.typer ===================================== --- /dev/null +++ b/samples/int_index_inconsistency.typer @@ -0,0 +1,10 @@ +% +% Int index inconsistency +% ------------------------------ +sqr = lambda (x : Int) -> x * x; +v = sqr 2; + +sqr2 : Int -> Int; +sqr2 = lambda x -> x * x; + +v2 = sqr2 2;
===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -57,6 +57,7 @@ let predef_name = [ "False"; "Bool"; "Macro"; + "expand_macro_"; ]
let builtin_size = ref 0 @@ -71,7 +72,7 @@ let predef_map = ref default_predef_map let get_predef_raw (name: string) : lexp = match !(SMap.find name (!predef_map)) with | Some exp -> exp - | None -> builtin_error dloc "Try to access an empty predefined" + | None -> builtin_error dloc ("""^ name ^ "" was not predefined")
let get_predef_option (name: string) ctx = let r = (get_size ctx) - !builtin_size - 1 in @@ -80,7 +81,7 @@ let get_predef_option (name: string) ctx = | None -> None
let get_predef (name: string) ctx = - let r = (get_size ctx) - !builtin_size - 1 in + let r = (get_size ctx) - !builtin_size - 0 in let p = get_predef_raw name in (mkSusp p (S.shift r))
@@ -157,12 +158,8 @@ let make_symbol loc depth args_val ctx =
(* lexp Imm list *) let olist2tlist_lexp lst ctx = - (* Get Constructor *) - let considx = senv_lookup "cons" ctx in - let nilidx = senv_lookup "nil" ctx in - - let tcons = Var((dloc, "cons"), considx) in - let tnil = Var((dloc, "nil"), nilidx) in + let tcons = get_predef "cons" ctx in + let tnil = get_predef "nil" ctx in
let rlst = List.rev lst in List.fold_left (fun tail elem -> @@ -191,8 +188,9 @@ let make_node loc depth args_val ctx =
let op, tlist = match args_val with | [Vsexp(op); lst] -> op, lst - | _ -> builtin_error loc - "node_ expects one 'Sexp' and one 'List Sexp'" in + | op::_ -> + builtin_error loc + ("node_ expects one 'Sexp' got " ^ (value_name op)) in
(* value_print tlist; print_string "\n"; *)
===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -61,6 +61,7 @@ type property_env = property_elem PropertyMap.t
(* easier to debug with type annotations *) type env_elem = (int * vdef option * varbind * ltype) +(* FIXME: This is the *lexp context*. *) type env_type = env_elem myers
type db_idx = int (* DeBruijn index. *) @@ -72,7 +73,14 @@ type scope = db_ridx StringMap.t (* Map<String, db_ridx>*) type senv_length = int (* it is not the map true length *) type senv_type = senv_length * scope
+(* FIXME: This is the *elaboration context* (i.e. a context that holds + * a lexp context plus some side info. *) type lexp_context = senv_type * env_type * property_env +type elab_context = lexp_context + +(* Extract the lexp context from the context used during elaboration. *) +let ectx_to_lctx (ectx : elab_context) : env_type = + let (_, lctx, _) = ectx in lctx
(* internal definitions * ---------------------------------- *) @@ -107,9 +115,20 @@ let env_extend (ctx: lexp_context) (def: vdef) (v: varbind) (t: lexp) = debruijn_warning loc ("Variable Shadowing " ^ name); with Not_found -> ()); let nmap = StringMap.add name n map in - (* FIXME: Why a db_offset of 1? *) - ((n + 1, nmap), cons (1, Some def, v, t) env, f) - + ((n + 1, nmap), cons (0, Some def, v, t) env, f) + +let ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) = + List.fold_left + (fun (ctx, recursion_offset) (def, e, t) -> + let (loc, name) = def in + let ((n, map), env, f) = ctx in + (try let _ = senv_lookup name ctx in + debruijn_warning loc ("Variable Shadowing " ^ name); + with Not_found -> ()); + let nmap = StringMap.add name n map in + ((n + 1, nmap), cons (recursion_offset, Some def, LetDef e, t) env, f), + recursion_offset - 1) + (ctx, List.length defs) defs
let _name_error loc estr str = if estr = str then () else @@ -144,7 +163,6 @@ let env_lookup_expr ctx (v : vref): lexp option = let (r, _, lxp, _) = _env_lookup ctx v in match lxp with | LetDef lxp -> Some (L.push_susp lxp (S.shift (idx + 1 - r))) - (* FIXME: why Sort here? *) | _ -> None
let env_lookup_by_index index (ctx: lexp_context): env_elem =
===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -264,19 +264,19 @@ and bind_impl loc depth args_val ctx =
let io, cb = match args_val with | [io; callback] -> io, callback - | _ -> builtin_error loc "bind expects two arguments" in + | _ -> eval_error loc "bind expects two arguments" in
(* build Vcommand from io function *) let cmd = match io with | Vcommand (cmd) -> cmd - | _ -> builtin_error loc "bind first arguments must be a monad" in + | _ -> eval_error loc "bind first arguments must be a monad" in
(* bind returns another Vcommand *) Vcommand (fun () -> (* get callback *) let body, ctx = match cb with | Closure(_, body, ctx) -> body, ctx - | _ -> builtin_error loc "A Closure was expected" in + | _ -> eval_error loc "A Closure was expected" in
(* run given command *) let underlying = cmd () in @@ -291,11 +291,11 @@ and run_io loc depth args_val ctx =
let io, ltp = match args_val with | [io; ltp] -> io, ltp - | _ -> builtin_error loc "run-io expects 2 arguments" in + | _ -> eval_error loc "run-io expects 2 arguments" in
let cmd = match io with | Vcommand (cmd) -> cmd - | _ -> builtin_error loc "run-io expects a monad as first argument" in + | _ -> eval_error loc "run-io expects a monad as first argument" in
(* run given command *) let _ = cmd () in
===================================== src/fmt.ml ===================================== --- a/src/fmt.ml +++ b/src/fmt.ml @@ -137,6 +137,20 @@ let print_first n l f = else () in loop 0 l
+let print_last n l f = + let len = List.length l in + let start = if (len - n) < 0 then 0 else (len - n) in + + let rec loop i l = + match l with + | [] -> () + | hd::tl -> + if (len > n) && (i <= start) then loop (i + 1) tl + else ((f i hd); loop (i + 1) tl) in + + loop 0 l + + (* Colors *) let red = "\x1b[31m" let green = "\x1b[32m"
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -121,6 +121,7 @@ and slookup s l v = S.lookup (fun l i -> Var (l, i)) s l v let ssink = S.sink (fun l i -> Var (l, i))
+ (**** The builtin elements ****) (* let builtins = @@ -329,7 +330,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) | Susp (e,s') -> push_susp e (scompose s' s) | (Var _ | Metavar _) -> nosusp (mkSusp e s)
-let nosusp e = (* Return `e` without `Susp`. *) +and nosusp e = (* Return `e` without `Susp`. *) match e with | Susp(e, s) -> push_susp e s | _ -> e @@ -495,6 +496,71 @@ let lexp_print e = sexp_print (pexp_unparse (lexp_unparse e)) *)
+(* ugly printing (sexp_print (pexp_unparse (lexp_to_pexp e))) *) +let rec lexp_to_pexp lxp = + match lxp with + | Susp _ as e -> lexp_to_pexp (nosusp e) + | Imm (sexp) -> Pimm (sexp) + | Builtin ((loc, name), _) -> Pvar((loc, name)) + | Var ((loc, name), _) -> Pvar((loc, name)) + | Cons (((iloc, iname), idx), ctor) -> Pcons((iloc, iname), ctor) + | Lambda (kind, vdef, ltp, body) -> + Plambda(kind, vdef, Some (lexp_to_pexp ltp), lexp_to_pexp body) + | Arrow (arg_kind, vdef, ltp1, loc, ltp2) -> + Parrow(arg_kind, vdef, lexp_to_pexp ltp1, loc, lexp_to_pexp ltp2) + + | Let (loc, ldecls, body) -> + (* (vdef * lexp * ltype) list *) + let pdecls = List.fold_left (fun acc (vdef, lxp, ltp) -> + Ptype(vdef, lexp_to_pexp ltp)::Pexpr(vdef, lexp_to_pexp lxp)::acc) [] ldecls in + Plet (loc, pdecls, lexp_to_pexp body) + + | Call(lxp, largs) -> (* (arg_kind * lexp) list *) + let pargs = List.map (fun (kind, elem) -> lexp_to_pexp elem) largs in + let sargs = List.map (fun elem -> pexp_unparse elem) pargs in + Pcall(lexp_to_pexp lxp, sargs) + + | Inductive(loc, label, lfargs, ctor) -> + (* (arg_kind * vdef * ltype) list *) + (* (arg_kind * pvar * pexp option) list *) + let pfargs = List.map (fun (kind, vdef, ltp) -> + (kind, vdef, Some (lexp_to_pexp ltp))) lfargs in + + (* ((arg_kind * vdef option * ltype) list) SMap.t *) + (* (symbol * (arg_kind * pvar option * pexp) list) list *) + let ctor = List.map (fun (str, largs) -> + let pargs = List.map (fun (kind, var, ltp) -> + match var with + | Some (loc, name) -> (kind, Some (loc, name), lexp_to_pexp ltp) + | None -> (kind, None, lexp_to_pexp ltp)) largs + in ((loc, str), pargs) + ) (SMap.bindings ctor) + in Pinductive(label, pfargs, ctor) + + | Case (loc, target, tltp, bltp, branches, default) -> + let pbranch = List.map (fun (str, (loc, args, bch)) -> + match args with + | [] -> Ppatvar (loc, str), lexp_to_pexp bch + | _ -> + let pat_args = List.map (fun (kind, vdef) -> + match vdef with + | Some vdef -> Some (kind, vdef), Ppatvar(vdef) + | None -> None, Ppatany(loc)) args + in Ppatcons ((loc, str), pat_args), lexp_to_pexp bch + ) (SMap.bindings branches) in + + let pbranch = match default with + | Some dft -> (Ppatany(loc), lexp_to_pexp dft)::pbranch + | None -> pbranch + in Pcase (loc, lexp_to_pexp target, pbranch) + + (* + | SortLevel of sort_level + | Sort of U.location * sort *) + + | _ as e -> Pimm (String(lexp_location e, "Type")) + + (* * Printing * --------------------- *) @@ -514,9 +580,29 @@ let pretty_ppctx = ref (true , 0, true, false, true, 4, true) let compact_ppctx = ref (false, 0, true, false, true, 4, false) let debug_ppctx = ref (false, 0, true, true , false, 4, true)
-let rec lexp_print e = _lexp_print (!debug_ppctx) e +let rec lexp_print e = _lexp_print (!debug_ppctx) e and _lexp_print ctx e = print_string (_lexp_to_str ctx e)
+(* +type print_context2 = int SMap.t + +let default_print_context = + List.fold (fun map (key, v) -> SMap.add key v map) + [ + (* true options *) + ("pretty", 1); + ("print_type", 1); + ("print_dbi", 1); + ("indent_size", 2); + ("color", 1); + ("separate_decl", 1); + + (* State information *) + ("indent_level", 0); + ("previous node", 0) + ] + SMap.empty *) + (* Print a lexp into its typer equivalent *) (* Depending on the print_context the output can be correct typer code *) (* This function will be very useful when debugging generated code *) @@ -525,8 +611,6 @@ and _lexp_print ctx e = print_string (_lexp_to_str ctx e) (* It might be better to use a Buffer. *) and lexp_to_str exp = _lexp_to_str (!debug_ppctx) exp
-(* FIXME: We don't want lexp_to_str, instead we want lexp_to_pexp (aka - * "unparse"), which we can then combine with pexp_to_sexp, etc... *) and _lexp_to_str ctx exp = (* create a string instead of printing *)
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -69,7 +69,6 @@ let lexp_fatal = msg_fatal "LPARSE" let _global_lexp_ctx = ref make_lexp_context let _global_lexp_trace = ref [] let _parsing_internals = ref false -let _shift_glob = ref 0 let btl_folder = ref "./btl/"
(* merged declaration, allow us to process declaration in multiple pass *) @@ -86,6 +85,22 @@ let _type_shift tp i = | Var(v, idx) -> Var(v, idx) | expr -> expr
+let ctx_define (ctx: lexp_context) var lxp ltype = + let (_, cctx, _) = ctx in + if OL.conv_p ltype (OL.check cctx lxp) then + env_extend ctx var (LetDef lxp) ltype + else + (print_string "¡¡ctx_define error!!\n"; + lexp_print lxp; + print_string " !: "; + lexp_print ltype; + print_string "\nbecause\n"; + lexp_print (OL.check cctx lxp); + print_string " != "; + lexp_print ltype; + print_string "\n"; + lexp_fatal (let (l,_) = var in l) "TC error") + (* The main job of lexp (currently) is to determine variable name (index) * and to regroup type specification with their variable * @@ -138,10 +153,6 @@ let mkMetavar () = let meta = Unif.create_metavar () in let name = "__Metavar_" ^ (string_of_int meta) in Metavar (meta, S.Identity, (Util.dummy_location, name))
-(* shift all variables by an offset *) -let senv_lookup name ctx = - senv_lookup name ctx + !_shift_glob - let rec lexp_p_infer (p : pexp) (ctx : lexp_context): lexp * ltype = _lexp_p_infer p ctx 1
@@ -228,7 +239,9 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = (* An inductive type named type_name must be in the environment *) try let idx = senv_lookup type_name ctx in (* Check if the constructor exists *) - let Some idt = env_lookup_expr ctx (vr, idx) in + let idt = match env_lookup_expr ctx (vr, idx) with + | Some idt -> idt + | None -> lexp_fatal loc ("expression " ^ type_name ^ " not found") in
(* make Base type *) let inductive_type = Var((loc, type_name), idx) in @@ -337,6 +350,9 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = let lxp, _ = lexp_case (Some t) (loc, target, patterns) ctx i in lxp
+ (* handle pcall here * ) + | Pcall (fname, _args) -> *) + | _ -> (let (e, inferred_t) = _lexp_p_infer p ctx (i + 1) in (* e *) match e with @@ -453,7 +469,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = | [] -> largs, ltp | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs (* Explicit-implicit argument. *) - -> (match OL.lexp_whnf ltp ctx meta_ctx with + -> (match OL.lexp_whnf ltp (ectx_to_lctx ctx) meta_ctx with | Arrow (ak, Some (_, aname'), arg_type, _, ret_type) when aname = aname' -> let parg = pexp_parse sarg in @@ -468,7 +484,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = ("Explicit-implicit arg " ^ aname ^ " to non-function")) | sarg :: sargs (* Process Argument *) - -> (match OL.lexp_whnf ltp ctx meta_ctx with + -> (match OL.lexp_whnf ltp (ectx_to_lctx ctx) meta_ctx with | Arrow (Aexplicit, _, arg_type, _, ret_type) -> let parg = pexp_parse sarg in let larg = _lexp_p_check parg arg_type ctx i in @@ -488,7 +504,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let handle_funcall () = (* Here we use lexp_whnf on actual code, but it's OK * because we only use the result when it's a "predefined constant". *) - match OL.lexp_whnf body ctx meta_ctx with + match OL.lexp_whnf body (ectx_to_lctx ctx) meta_ctx with | Builtin((_, "Built-in"), _) -> ( (* ------ SPECIAL ------ *) @@ -520,27 +536,16 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = Call (body, List.rev largs), ret_type in
let handle_macro_call () = - (* FIXME: We shouldn't look at `body` here at all: - * Instead, we should pass `body` (along with `arg`) to - * a `typer__expand_macro` function predefined in types.typer. *) - let lxp = match OL.lexp_whnf body ctx meta_ctx with - | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct - | lxp -> - print_string "\n"; - print_string (lexp_to_string lxp); print_string "\n"; - lexp_print lxp; print_string "\n"; - lexp_fatal loc "Macro is ill formed" in - (* Build function to be called *) - let arg = olist2tlist_lexp sargs ctx in - - let lxp = Call(lxp, [(Aexplicit, arg)]) in - let elexp = OL.erase_type lxp in + let macro_expand = get_predef "expand_macro_" ctx in + let args = [(Aexplicit, body); (Aexplicit, (olist2tlist_lexp sargs ctx))] in + let macro = Call(macro_expand, args) in + let emacro = OL.erase_type macro in let rctx = (from_lctx ctx 0) in
_global_eval_trace := [];
- let vxp = try eval elexp rctx + let vxp = try eval emacro rctx with e -> print_eval_trace (); raise e in @@ -552,7 +557,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = | Vstring(s) -> String(dloc, s) | Vfloat(f) -> Float(dloc, f) (* I have vdum here WHY *) - | v -> debug_msg (value_print v); + | v -> debug_msg (value_print v); print_string "\n"; lexp_fatal loc "Macro_ expects '(List Sexp) -> Sexp'" in
let pxp = pexp_parse sxp in @@ -567,10 +572,12 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i =
(* determine function type *) match func, ltp with + (* FIXME: this branch is never used because of missing shift somewhere *) + (* while special form have a type macro this does not recognize them as such *) | macro, _ when OL.conv_p ltp macro_type -> ( match macro with - (* Special form *) | Pvar(l, name) when is_builtin_macro name -> + print_string name; let pargs = List.map pexp_parse sargs in let largs = _lexp_parse_all pargs ctx i in (get_macro_impl loc name) loc largs ctx ltp @@ -581,6 +588,21 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = (* FIXME: Handle special-forms here as well! *) | _ -> handle_funcall ()
+(* return the inductive type declaration from the constructor *) +and lexp_get_inductive_type loc ctor_name ctx : (string * lexp option) = + let cons_idx = senv_lookup ctor_name ctx in + let cons = match env_lookup_expr ctx ((loc, ctor_name), cons_idx) with + | Some lxp -> lxp + | None -> lexp_warning loc ("constructor "" ^ ctor_name ^ "" not found"); dltype in + + (* get inductive type index *) + match cons with + | Cons(((_, name), idx), _) -> + (* get inductive type declaration *) + name, env_lookup_expr ctx ((loc, name), idx + cons_idx) + + | _ -> lexp_warning loc (ctor_name ^ " is not a constructor"); + "", None
(* Read a pattern and create the equivalent representation *) and lexp_read_pattern pattern exp target ctx: @@ -600,43 +622,78 @@ and lexp_read_pattern pattern exp target ctx: (* name is defined but is not a constructor *) (* it technically could be ... (expr option) *) (* What about Var -> Cons ? *) - | _ -> let nctx = env_extend ctx var (LetDef target) dltype in + | _ -> let nctx = ctx_define ctx var target dltype in (name, loc, []), nctx)
(* would it not make a default match too? *) with Not_found -> (* Create a variable containing target *) - let nctx = env_extend ctx var (LetDef target) dltype in + let nctx = ctx_define ctx var target dltype in (name, loc, []), nctx)
| Ppatcons (ctor_name, args) -> - let (loc, name) = ctor_name in + let (loc, cons_name) = ctor_name in + + (* We need the constructor type info *) + let inductive_name, inductive_ref = match lexp_get_inductive_type loc cons_name ctx with + | name, Some lxp -> name, lxp + | _ -> "", dltype in + + (*get cons argument types *) + let cons_args = match inductive_ref with + | Inductive(_, _, _, map) -> (try SMap.find cons_name map + with Not_found -> lexp_warning loc + (inductive_name ^ " does not hold a " ^ cons_name ^ " constructor"); []) + | _ -> [] in + + (* remove non explicit argument *) + let rec remove_nexplicit args acc = + match args with + | [] -> List.rev acc + | (Aexplicit, _, ltp)::tl -> remove_nexplicit tl (ltp::acc) + | hd::tl -> remove_nexplicit tl acc in + + let cons_args = remove_nexplicit cons_args [] in
(* read pattern args *) - let args, nctx = lexp_read_pattern_args args ctx in - (name, loc, args), nctx + let args, nctx = lexp_read_pattern_args args cons_args ctx in + (cons_name, loc, args), nctx
(* Read patterns inside a constructor *) -and lexp_read_pattern_args args ctx: +and lexp_read_pattern_args args (args_type : lexp list) ctx: (((arg_kind * vdef option) list) * lexp_context)=
- let rec loop args acc ctx = - match args with - | [] -> (List.rev acc), ctx - | hd::tl -> ( + let length_type = List.length args_type in + let length_pat = List.length args in + + let make_list elem size = + let rec loop i acc = + if i < size then loop (i + 1) (elem::acc) else acc + in loop 0 [] in + + let args_type = if length_type != length_pat then + make_list dltype length_pat else args_type in + + (if length_type != length_pat then lexp_warning dloc "Size Mismatch"); + + let rec loop args args_type acc ctx = + match args, args_type with + | [], _ -> (List.rev acc), ctx + | hd::tl, ltp::type_tl -> ( let (_, pat) = hd in match pat with (* Nothing to do *) - | Ppatany (loc) -> loop tl ((Aexplicit, None)::acc) ctx + | Ppatany (loc) -> loop tl type_tl ((Aexplicit, None)::acc) ctx | Ppatvar ((loc, name) as var) -> (* Add var *) - let nctx = env_extend ctx var Variable dltype in + let nctx = env_extend ctx var Variable ltp in let nacc = (Aexplicit, Some var)::acc in - loop tl nacc nctx + loop tl type_tl nacc nctx | _ -> lexp_error dloc "Constructor inside a Constructor"; - loop tl ((Aexplicit, None)::acc) ctx) + loop tl type_tl ((Aexplicit, None)::acc) ctx) + | _ -> typer_unreachable "unreachable branch"
- in loop args [] ctx + in loop args args_type [] ctx
(* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx i = @@ -681,6 +738,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) = (* get stored function *) let lxp = match lxp with | Some (Call(Var((_, "Macro_"), _), [(_, fct)])) -> fct + | None -> lexp_fatal loc "expression does not exist" | Some lxp -> print_string "\n"; print_string (lexp_to_string lxp); print_string "\n"; lexp_print lxp; print_string "\n"; @@ -712,8 +770,6 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) = (* get a list of declaration *) let decls = eval elexp rctx in
- value_print decls; print_string "\n"; - (* convert typer list to ocaml *) let decls = tlist2olist [] decls in
@@ -832,7 +888,7 @@ and _lexp_decls decls ctx i: ((vdef * lexp * ltype) list list * lexp_context) = (List.rev !all), ctx
and _lexp_rec_decl decls ctx i = - (* parse a groupe of mutually recursive definition + (* parse a group of mutually recursive definitions * i.e let decl parsing *)
(* to compute recursive offset *) @@ -840,8 +896,8 @@ and _lexp_rec_decl decls ctx i = let lst = ref [] in
(* add all elements to the environment *) - let tctx = List.fold_left (fun vctx expr -> - match expr with + let tctx = List.fold_left (fun vctx decl -> + match decl with | Ldecl((l, s), _, None) -> env_extend vctx (l, s) ForwardRef dltype
@@ -853,9 +909,9 @@ and _lexp_rec_decl decls ctx i = lexp_fatal dloc "use lexp_decl_macro to parse macro decls") ctx decls in
let i = ref 0 in - let ctx = List.fold_left (fun vctx expr -> + let ctx = List.fold_left (fun vctx decl -> i := !i + 1; - match expr with + match decl with (* lexp infer *) | Ldecl ((l, s), Some pxp, None) -> let lxp, ltp = lexp_p_infer pxp vctx in @@ -1002,11 +1058,11 @@ let default_lctx, default_rctx =
(* Empty context *) let lctx = make_lexp_context in - let lctx = env_extend lctx (dloc, "Type1") (LetDef type1) type2 in - let lctx = env_extend lctx (dloc, "Type") (LetDef type0) type1 in + let lctx = ctx_define lctx (dloc, "Type1") type1 type2 in + let lctx = ctx_define lctx (dloc, "Type") type0 type1 in (* FIXME: Add builtins directly here. *) let lxp = Builtin((dloc, "Built-in"), type0) in - let lctx = env_extend lctx (dloc, "Built-in") (LetDef lxp) type0 in + let lctx = ctx_define lctx (dloc, "Built-in") lxp type0 in
(* Read BTL files *) let pres = prelex_file (!btl_folder ^ "types.typer") in
===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -39,6 +39,21 @@ module DB = Debruijn
let conv_erase = true (* If true, conv ignores erased terms. *)
+(* Lexp context *) + +type lexp_context = DB.env_type + +let lookup_type (ctx : lexp_context) vref = + let (_, i) = vref in + let (_, _, _, t) = Myers.nth i ctx in + mkSusp t (S.shift (i + 1)) + +let lookup_value (ctx : lexp_context) vref = + let (_, i) = vref in + match Myers.nth i ctx with + | (o, _, LetDef v, _) -> Some (push_susp v (S.shift (i + 1 - o))) + | _ -> None + (********* Testing if two types are "convertible" aka "equivalent" *********)
let rec conv_arglist_p s1 s2 args1 args2 : bool = @@ -56,7 +71,7 @@ and conv_p' (s1:lexp S.subst) (s2:lexp S.subst) e1 e2 : bool = | (Imm (Float (_, i1)), Imm (Float (_, i2))) -> i1 = i2 | (Imm (String (_, i1)), Imm (String (_, i2))) -> i1 = i2 | (SortLevel (sl1), SortLevel (sl2)) -> sl1 == sl2 - | (Sort (_, s1), Sort (_, s2)) -> s1 == s2 + | (Sort (_, s1), Sort (_, s2)) -> s1 = s2 | (Builtin ((_, s1), _), Builtin ((_, s2), _)) -> s1 == s2 (* BEWARE: When we'll make expand let-defined vars here, we'll have to * be careful not to introduce infinite-recursion. *) @@ -118,7 +133,7 @@ and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2 * but only on *types*. If you must use it on code, be sure to use its * return value as little as possible since WHNF will inherently introduce * call-by-name behavior. *) -let rec lexp_whnf e ctx meta_ctx = +let rec lexp_whnf e (ctx : lexp_context) meta_ctx = Debug_fun.do_debug (fun () -> prerr_endline ("[StackTrace] ------------------------------------------"); prerr_endline ("[StackTrace] let lexp_whnf e ctx meta_ctx"); @@ -129,7 +144,7 @@ let rec lexp_whnf e ctx meta_ctx = ()); match e with (* | Let (_, defs, body) -> FIXME!! Need recursive substitutions! *) - | Var v -> (match DB.env_lookup_expr ctx v with + | Var v -> (match lookup_value ctx v with | None -> e (* We can do this blindly even for recursive definitions! * IOW the risk of inf-looping should only show up when doing @@ -178,17 +193,6 @@ let rec lexp_whnf e ctx meta_ctx = (********* Testing if a lexp is properly typed *********)
-let lookup_type ctx vref = - let (_, i) = vref in - let (_, _, _, t) = Myers.nth i ctx in - mkSusp t (S.shift (i + 1)) - -let lookup_value ctx vref = - let (_, i) = vref in - match Myers.nth i ctx with - | (o, _, LetDef v, _) -> Some (push_susp v (S.shift (i + 1 - o))) - | _ -> None - let assert_type e t t' = if conv_p t t' then () else U.msg_error "TC" (lexp_location e) "Type mismatch"; () @@ -212,7 +216,7 @@ let rec check ctx e = match e with | Imm (Float (_, _)) -> B.type_float | Imm (Integer (_, _)) -> B.type_int - | Imm (Epsilon|Block (_, _, _)|Symbol _|String (_, _)|Node (_, _)) + | Imm (Epsilon | Block (_, _, _) | Symbol _ | String (_, _) | Node (_, _)) -> (U.msg_error "TC" (lexp_location e) "Unsupported immediate value!"; B.type_int) | SortLevel (_) -> B.type_level
===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -112,7 +112,7 @@ let print_trace name max elem_to_string print_elem trace = print_string (Fmt.make_sep '-');
let racc = List.rev trace in - Fmt.print_first max racc (fun j (i, l, g) -> + Fmt.print_last max racc (fun j (i, l, g) -> print_string " ["; print_loc l; print_string "] "; Fmt._print_ct_tree i; print_string "+- "; print_string (elem_to_string g); print_string ": ";
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -375,6 +375,46 @@ let _ = (add_test "EVAL" "List" (fun () -> ))
+let _ = (add_test "EVAL" "Monads" (fun () -> + reset_eval_trace (); + + let dcode = " + c = bind (a := Type) (b := Type) (open "./_build/w_file.txt" "w") + (lambda (f : FileHandle) -> + write f "Hello2"); + + " in + + let rctx, lctx = eval_decl_str dcode lctx rctx in + + let rcode = "run-io (a := Type) (b := Unit) c Unit" in + + (* Eval defined lambda *) + let ret = eval_expr_str rcode lctx rctx in + (* Expect a 3 results *) + match ret with + | [v] -> success () + | _ -> failure () +)) + +(* +let test_eval_eqv decl run expected_result = + add_test "EVAL" dcode1 (fun () -> + + let rctx, lctx = eval_decl_str decl lctx rctx in + + let result = eval_expr_str rcode lctx rctx + let expected_result = eval_expr_str expected_result lctx rctx + + if sexp_eq_list result expected_result + then success () + else ( + value_print (List.hd s1); + value_print (List.hd s2); + failure ())) + +*) + (* run all tests *) let _ = run_all ()
View it on GitLab: https://gitlab.com/monnier/typer/compare/2bd4d49a243a0d575615a8f09942a3687ad...