Les équations fonctionnent !

bin/main.ml

@@ -6,7 +6,7 @@ open Linear_intf
 open Reduction_intf
 open TypeInfer_intf
 
-let version = "v0.0.3-alpha"
+let version = "v0.0.4-alpha"
 
 let usage_spiel =
   {|usage: autobill [options] [input_file]|}

eqns_pack.bill

+decl sort idx
+
+decl type f : (idx -> (idx -> idx))
+
+decl type carrier : (idx -> (idx -> +))
+
+decl type x0 : idx
+
+decl type y0 : idx
+
+pack foo_t (a : idx) (b : idx) =
+  foo[(x : idx), (y : idx)]((carrier x y))
+  with x = (f y a), y = (f x b)
+
+decl val foor : (carrier x0 y0)
+
+val fooz = foo[x0,y0](foor)
+

eqns_spec.bill

+decl sort idx
+
+decl type carrier : (idx -> (idx -> -))
+
+spec bar_aux_t =
+  this.bar_aux[(x : idx), (y : idx)]().ret(): (carrier x y)
+  with x = y
+
+spec bar_t =
+  this.bar[(x:idx)]().ret(): (carrier x x)
+
+decl val baz_aux : bar_aux_t
+
+val bazz = match this.bar[x1:idx]().ret(a) ->
+  baz_aux.bar_aux[x1,x1]().ret(a)

lib/Intern/intern_prelude.ml

@@ -302,15 +302,15 @@ let sort_check_one_item env item =
 
 | Pack_definition { name; args; cons; private_typs; arg_typs; equations; loc } ->
   let new_name = StringEnv.find name env.tycons_vars in
-    let new_env, new_scope, new_private, new_args =
+    let env, new_scope, new_private, new_args =
       sort_check_tycons_args env scope ~priv:private_typs args in
   if StringEnv.mem cons env.conses then
      fail_double_def ("constructor " ^ cons) loc;
    let arg_typs = List.map
-       (fun typ -> sort_check_type loc new_env sort_postype
-           (intern_type new_env new_scope typ))
+       (fun typ -> sort_check_type loc env sort_postype
+           (intern_type env new_scope typ))
        arg_typs in
-   let equations = List.map (sort_check_eqn loc env scope) equations in
+   let equations = List.map (sort_check_eqn loc env new_scope) equations in
    let new_cons = ConsVar.of_string cons in
    let cons_def = Consdef {
        typ_args = new_args;
@@ -351,7 +351,7 @@ let sort_check_one_item env item =
        arg_typs in
    let ret_typ = sort_check_type loc env sort_negtype
        (intern_type env new_scope ret_typ) in
-   let equations = List.map (sort_check_eqn loc env scope) equations in
+   let equations = List.map (sort_check_eqn loc env new_scope) equations in
    let new_destr = DestrVar.of_string destr in
    let destr_def = Destrdef {
        typ_args = new_args;

lib/TypeInfer/TypeInfer_intf.ml

@@ -17,7 +17,7 @@ let constraint_as_string (prelude, items) =
 let post_contraint_as_string (prelude, _, post) =
   let module P = struct let it = prelude end in
   let open Elaborate.Make(P) in
-  let post = FirstOrder.compress_logic post in
+  let post = FOLNormalize.normalize post in
   let string_of_type t =
     PrettyPrinter.pp_typ Format.str_formatter t;
     Format.flush_str_formatter () in

lib/TypeInfer/constraint.ml

@@ -10,8 +10,6 @@ module Make (U : Unifier_params) = struct
 
   include UnionFind.Make (U)
 
-  type 'a post_con = (sort, rel, 'a, 'a) formula
-
   let existentials = ref []
 
   let model = ref []
@@ -160,15 +158,17 @@ module Make (U : Unifier_params) = struct
 
   let _trace stack con post =
     buffer ();
-    print_endline "\n** context";
+    print_endline "** context";
     print_sexpr (kontext_to_sexpr stack);
-    print_endline "\n** constraint";
+    print_endline "** constraint";
     print_sexpr (con_to_sexpr uvar_to_sexpr con);
-    print_endline "\n** post";
+    print_endline "** post";
+    print_sexpr (S (List.map uvar_to_sexpr !existentials));
+    print_sexpr (eqns_to_sexpr U.string_of_rel uvar_to_sexpr !model);
     print_sexpr (post_con_to_sexpr rel_to_sexpr uvar_to_sexpr uvar_to_sexpr post);
-    print_endline "\n** env";
+    print_endline "** env";
     print_sexpr (_env_to_sexpr ());
-    print_endline "\n** unification";
+    print_endline "** unification";
     print_sexpr (subst_to_sexpr !_state)
 
     let rec compress_cand c =
@@ -236,9 +236,9 @@ module Make (U : Unifier_params) = struct
       | KDef (x,a,ctx) -> KDef (x,a, go ctx)
       | KLet1 lett->
         KLet1 {lett with
-               accumulated = us @ lett.accumulated;
-               existentials = idx @ lett.existentials;
-               exist_eqns = eqns @ lett.exist_eqns}
+               accumulated = List.fold_left insert_nodup us lett.accumulated;
+               existentials = List.fold_left insert_nodup idx lett.existentials;
+               exist_eqns =  List.fold_left insert_nodup eqns lett.exist_eqns}
       | KLet2 lett -> KLet2 {lett with outer = go lett.outer} in
     go stack
 
@@ -252,9 +252,9 @@ module Make (U : Unifier_params) = struct
 
 
 
-  let finalize_post_con env (c : uvar post_con) =
-    let model x = Eq (deep_of_var (env.get x), env.u x, get_sort x) in
-    let finalize_eqns = List.map (function
+  let finalize_post_con env c : (sort, rel, var, deep) formula =
+    let model_id x = Eq (deep_of_var (env.get x), env.u x, get_sort x) in
+    let finalize_eqns  = List.map (function
       | Eq (a, b, so) -> Eq (env.u a, env.u b, so)
       | Rel (rel, args) -> Rel (rel, List.map env.u args)) in
     let rec go = function
@@ -263,12 +263,18 @@ module Make (U : Unifier_params) = struct
       | PLoc (loc, c) -> PLoc (loc, go c)
       | PEqn eqns -> PEqn (finalize_eqns eqns)
       | PAnd cs -> PAnd (List.map go cs)
-      | PExists (vars, [], c) ->
-        PExists (List.map env.get vars, List.map model vars, go c)
-      | PForall (vars, [], c) ->
-        PForall (List.map env.get vars, List.map model vars, go c)
-      | _ -> raise (Invalid_argument "") in
-    go c
+      | PExists (vars, eqns, c) ->
+        PExists (List.map env.get vars,
+                 List.map model_id vars @ finalize_eqns eqns,
+                 go c)
+      | PForall (vars, eqns, c) ->
+        PForall (List.map env.get vars,
+                 List.map model_id vars @finalize_eqns eqns,
+                 go c) in
+    let existentials = List.fold_left insert_nodup [] (List.map repr !existentials) in
+    PExists (List.map env.get existentials,
+             finalize_eqns !model @ List.map model_id existentials,
+             go c)
 
   let solve ?trace:(do_trace=false) (elab : 'a elaboration) (x : 'a) =
 
@@ -282,7 +288,7 @@ module Make (U : Unifier_params) = struct
       let post = finalize_post_con env post in
       gen env, post
 
-   and advance stack con : uvar post_con =
+   and advance stack con =
       if do_trace then _trace stack con PTrue;
       match con with
 
@@ -316,7 +322,7 @@ module Make (U : Unifier_params) = struct
                            univ_eqns; exist_eqns} in
         advance stack inner
 
-    and backtrack stack post : uvar post_con =
+    and backtrack stack post =
       if do_trace then _trace stack CTrue post;
       match stack with
 
@@ -353,7 +359,7 @@ module Make (U : Unifier_params) = struct
         Array.iteri lift_freevars (ranked_freevars_of_scheme scheme !_rank);
         (* We now know which vars can be lifted in the surronding scope! *)
         let scheme, old = extract_old_vars scheme !_rank in
-        let xs = List.map repr accumulated and ys = List.map repr quantification_duty in
+        let xs = List.map repr (fst scheme) and ys = List.map repr quantification_duty in
         if not (is_sublist ys xs) then
           raise (Not_sufficiently_polymorphic var);
           tmp "After lifting scheme" scheme;
@@ -364,6 +370,8 @@ module Make (U : Unifier_params) = struct
         generalize var gen scheme;
 
         let existentials = List.map repr existentials in
+        let existentials = List.fold_left insert_nodup [] existentials in
+        let existentials = List.filter (fun x -> not (List.mem x (fst scheme))) existentials in
         let ctx = KLet2 {var; typ; quantified = accumulated;
                          outer=inner'; eqns = univ_eqns} in
         let post' = advance ctx outer in

lib/TypeInfer/constraints_params.ml

@@ -104,7 +104,7 @@ module Params (Prelude : Prelude) = struct
     let string_of_var = string_of_tvar
     let var_of_string = tvar_of_string
 
-    let deep_of_var s = tvar s
+    let deep_of_var s = TInternal s
 
     let mk_var () =
       let s = Global_counter.fresh "a" in

lib/TypeInfer/unionFind.ml

@@ -411,10 +411,9 @@ module Make (P : Unifier_params) = struct
   let specialize spec vs : unit =
     _specializers := (spec, vs) :: !_specializers
 
-  type generalizer = (var list * deep) ref
-  let _gens :
-    (generalizer * uvar list * uvar) list ref = ref []
-  let new_gen () = ref ([], deep_of_var (mk_var ()))
+  type generalizer = (var list * deep) option ref
+  let _gens : (generalizer * uvar list * uvar) list ref = ref []
+  let new_gen () = ref None
   let generalize _ gen (us, u) =
     _gens := (gen, us, u) :: !_gens
 
@@ -453,7 +452,7 @@ module Make (P : Unifier_params) = struct
 
     let env_scheme (us,u) = (List.map get us, aux u) in
     let spec_aux (spec, vs) = spec := List.map aux vs in
-    let gen_aux (gen, us, u) = gen := env_scheme (us, u) in
+    let gen_aux (gen, us, u) = gen := Some (env_scheme (us, u)) in
     List.iter spec_aux !_specializers;
     List.iter gen_aux !_gens;
     {

lib/firstOrder.ml

@@ -76,67 +76,3 @@ let rec map f_var f_term = function
   | PForall (xs, eqns, c) ->
 
     PForall (List.map f_var xs, map_eqns f_term eqns, map f_var f_term c)
-
-type ('sort, 'rel, 'var, 'term) compress_quantifiers_t =
-  | Univ of 'var list * ('sort, 'rel, 'term) eqn list
-  | Exist of 'var list * ('sort, 'rel, 'term) eqn list
-
-
-let rec compress_logic c =
-
-  let canary = ref false in
-
-  let kill () = (canary := true) in
-
-  let rec advance c ctx = match c with
-    | PTrue | PEqn [] -> shortcut_true ctx
-    | PFalse -> shortcut_false ctx
-    | PEqn _ -> backtrack c ctx
-    | PLoc (loc, c) -> advance c (lift_loc loc ctx)
-    | PAnd [] -> backtrack PTrue ctx
-    | PAnd (x::xs) -> advance x (lift_and xs ctx)
-    | PExists (vs, eqns, x) -> advance x (lift_quant (Exist (vs, eqns)) ctx)
-    | PForall (vs, eqns, x) -> advance x (lift_quant (Univ (vs,eqns)) ctx)
-
-  and backtrack c ctx = match ctx with
-    | KEmpty -> c
-    | KLoc (loc, ctx) -> backtrack (PLoc (loc, c)) ctx
-    | KAnd ([], ctx, []) -> kill (); backtrack c ctx
-    | KAnd (xs, ctx, []) -> backtrack (PAnd (c::xs)) ctx
-    | KAnd (xs, ctx, y::ys) -> advance y (KAnd (c::xs, ctx, ys))
-    | KForall (vs, eqns, ctx) -> backtrack (PForall (vs, eqns, c)) ctx
-    | KExists (vs, eqns, ctx) -> backtrack (PExists (vs, eqns, c)) ctx
-
-  and lift_loc loc = function
-    | KLoc (_, ctx) -> kill (); KLoc (loc, ctx)
-    | ctx -> KLoc (loc, ctx)
-
-  and lift_quant vs ctx = match vs,ctx with
-    | Exist (vs, eqns), KExists (vs', eqns', ctx') ->
-      kill (); KExists (vs@vs', eqns@eqns', ctx')
-    | Univ (vs, eqns), KForall (vs', eqns', ctx') ->
-      kill (); KForall (vs@vs', eqns@eqns', ctx')
-    | Exist (vs, eqns), _ -> KExists (vs, eqns, ctx)
-    | Univ (vs, eqns), _ -> KForall (vs, eqns, ctx)
-
-  and lift_and cs ctx = match ctx with
-    | KAnd (xs, ctx, ys) -> kill (); KAnd (xs, ctx, cs @ ys)
-    | ctx -> KAnd ([], ctx, cs)
-
-  and shortcut_false ctx = match ctx with
-    | KEmpty -> PFalse
-    | KLoc (_, ctx)
-    | KAnd (_, ctx, _)
-    | KExists (_, _, ctx) -> kill (); shortcut_false ctx
-    | KForall _ -> backtrack PFalse ctx
-
-  and shortcut_true ctx = match ctx with
-    | KEmpty -> PTrue
-    | KLoc (_, ctx)
-    | KForall (_, _, ctx) -> kill (); shortcut_true ctx
-    | KAnd (xs, ctx, []) -> backtrack (PAnd xs) ctx
-    | KAnd (xs, ctx, y::ys) -> advance y (KAnd (xs, ctx, ys))
-    | KExists _ -> backtrack PTrue ctx in
-
-  let c = advance c KEmpty in
-  if !canary then compress_logic c else c

lib/prettyPrinter.ml

@@ -40,7 +40,7 @@ let rec pp_typ fmt t =
   | TPos t -> fprintf fmt "+%a" pp_typ t
   | TNeg t -> fprintf fmt "-%a" pp_typ t
   | TVar v -> pp_tyvar fmt v.node
-  | TInternal v -> fprintf fmt "%a" pp_tyvar v
+  | TInternal v -> pp_tyvar fmt v
   | TBox b -> fprintf fmt "@[<hov 2>(%s@ %a)@]" (string_of_box_kind b.kind) pp_typ b.node
   | TFix t -> fprintf fmt "@[<hov 2>(fix@ %a)@]" pp_typ t
   | TCons {node;_} -> pp_print_string fmt (string_of_type_cons TyConsVar.to_string node)