minor fixes

src/compiler/compiler.ml

@@ -71,21 +71,17 @@ module SymbolMap : sig
   val global_name : D.State.t -> table -> constant -> F.t
   val compile : table -> D.symbol_table
   val compile_s2c : table -> (constant * D.term) F.Map.t
-  val compile_c2mode : table -> constant -> Mode.hos
 
 end = struct
 
   type table = {
     ast2ct : (constant * D.term) F.Map.t;
     c2t : D.term Constants.Map.t;
     c2s : string Constants.Map.t;
-    c2mode : Mode.hos Constants.Map.t;
     last_global : int;
   }
   [@@deriving show, ord]
 
-  let compile_c2mode t k = Util.Constants.Map.find k t.c2mode
-
   let equal_globals m1 m2 = m1.last_global = m2.last_global
 
 
@@ -105,7 +101,7 @@ end = struct
 
   let compile_s2c { ast2ct } = ast2ct
 
-  let allocate_global_symbol_aux x ({ c2t; c2s; ast2ct; last_global; c2mode } as table) =
+  let allocate_global_symbol_aux x ({ c2t; c2s; ast2ct; last_global } as table) =
     try table, F.Map.find x ast2ct
     with Not_found ->
       let last_global = last_global - 1 in
@@ -115,8 +111,7 @@ end = struct
       let c2t = Util.Constants.Map.add n xx c2t in
       let ast2ct = F.Map.add x p ast2ct in
       let c2s = Util.Constants.Map.add n (F.show x) c2s in
-      let c2mode = Util.Constants.Map.add n [] c2mode in
-      { c2t; c2s; ast2ct; last_global; c2mode }, p
+      { c2t; c2s; ast2ct; last_global }, p
 
   let get_global_symbol { ast2ct } s =
     try
@@ -135,7 +130,6 @@ end = struct
       let s = F.from_string s in
       let _, t = F.Map.find s D.Global_symbols.(table.s2ct) in
       t) D.Global_symbols.(table.c2s);
-    c2mode = D.Global_symbols.(table.c2mode);
   } in
   (*T2.go allocate_global_symbol_aux*) table
 
@@ -217,7 +211,7 @@ module C = Constants
 
 open Compiler_data
 
-module IDPosUf = IdPos.UF
+module UF = IdPos.UF
 
 type macro_declaration = (ScopedTerm.t * Loc.t) F.Map.t
 [@@ deriving show, ord]
@@ -255,7 +249,7 @@ type unchecked_signature = {
   kinds : Arity.t F.Map.t;
   types : TypeList.t F.Map.t;
   type_abbrevs : (F.t * ScopedTypeExpression.t) list;
-  type_uf : IDPosUf.t
+  type_uf : UF.t
 }
 [@@deriving show]
 
@@ -278,7 +272,7 @@ module Assembled = struct
     types : TypeAssignment.overloaded_skema_with_id F.Map.t;
     type_abbrevs : (TypeAssignment.skema_w_id * Loc.t) F.Map.t;
     functional_preds: Determinacy_checker.t;
-    type_uf : IDPosUf.t
+    type_uf : UF.t
   }
   [@@deriving show]
 
@@ -306,9 +300,9 @@ module Assembled = struct
   let empty_signature () = {
     kinds = F.Map.empty;
     types = F.Map.empty;
-    type_abbrevs = F.Map.empty; functional_preds = Determinacy_checker.empty_fmap;
+    type_abbrevs = F.Map.empty; functional_preds = Determinacy_checker.empty;
     toplevel_macros = F.Map.empty;
-    type_uf = IDPosUf.empty
+    type_uf = UF.empty
   }
   let empty () = {
     clauses = [];
@@ -402,6 +396,8 @@ type query = WithMain.query
   Compiler
  ****************************************************************************)
 
+let valid_functional = function [] -> Some Ast.Structured.Relation | [Ast.Functional] -> Some Function | _ -> None
+
 module RecoverStructure : sig
 
   (* Reconstructs the structure of the AST (i.e. matches { with }) *)
@@ -527,8 +523,6 @@ end = struct (* {{{ *)
     | [] -> { Type.attributes = (); loc; name; ty }
     | x :: _ -> error ~loc ("illegal attribute " ^ show_raw_attribute x)
 
-  let valid_functional = function [] -> Some Relation | [Functional] -> Some Function | _ -> None
-
   let structure_type_attributes { Type.attributes; loc; name; ty } =
     let duplicate_err s =
       error ~loc ("duplicate attribute " ^ s) in
@@ -900,14 +894,14 @@ end = struct
           else ScopedTerm.App(Scope.mkGlobal (), c, x, xs)
     | Cast (t,ty) ->
         let t = scope_loc_term ~state ctx t in
-        let ty = scope_loc_tye F.Set.empty (RecoverStructure.structure_type_expression ty.Ast.TypeExpression.tloc Ast.Structured.Relation (function [] -> Some Ast.Structured.Relation | _ -> None) ty) in
+        let ty = scope_loc_tye F.Set.empty (RecoverStructure.structure_type_expression ty.Ast.TypeExpression.tloc Ast.Structured.Relation valid_functional ty) in
         ScopedTerm.Cast(t,ty)
     | Lam (c,ty,b) when is_discard c ->
-        let ty = ty |> Option.map (fun ty -> scope_loc_tye F.Set.empty (RecoverStructure.structure_type_expression ty.Ast.TypeExpression.tloc Ast.Structured.Relation (function [] -> Some Ast.Structured.Relation | _ -> None) ty)) in
+        let ty = ty |> Option.map (fun ty -> scope_loc_tye F.Set.empty (RecoverStructure.structure_type_expression ty.Ast.TypeExpression.tloc Ast.Structured.Relation valid_functional ty)) in
         ScopedTerm.Lam (None,ty,ScopedTerm.mk_empty_lam_type None, scope_loc_term ~state ctx b)
     | Lam (c,ty,b) ->
         if has_dot c then error ~loc "Bound variables cannot contain the namespaec separator '.'";
-        let ty = ty |> Option.map (fun ty -> scope_loc_tye F.Set.empty (RecoverStructure.structure_type_expression ty.Ast.TypeExpression.tloc Ast.Structured.Relation (function [] -> Some Ast.Structured.Relation | _ -> None) ty)) in
+        let ty = ty |> Option.map (fun ty -> scope_loc_tye F.Set.empty (RecoverStructure.structure_type_expression ty.Ast.TypeExpression.tloc Ast.Structured.Relation valid_functional ty)) in
         let name = Some (c,elpi_language) in
         ScopedTerm.Lam (name,ty, ScopedTerm.mk_empty_lam_type name,scope_loc_term ~state (F.Set.add c ctx) b)
     | CData c -> ScopedTerm.CData c (* CData.hcons *)
@@ -1106,10 +1100,10 @@ module Flatten : sig
     Arity.t F.Map.t ->
     Arity.t F.Map.t
   val merge_type_assignments :
-    IDPosUf.t ->
+    UF.t ->
     TypeAssignment.overloaded_skema_with_id F.Map.t ->
     TypeAssignment.overloaded_skema_with_id F.Map.t ->
-    IdPos.t list * IDPosUf.t * TypeAssignment.overloaded_skema_with_id F.Map.t
+    IdPos.t list * UF.t * TypeAssignment.overloaded_skema_with_id F.Map.t
   val merge_type_abbrevs :
     (F.t * ScopedTypeExpression.t) list ->
     (F.t * ScopedTypeExpression.t) list ->
@@ -1119,10 +1113,10 @@ module Flatten : sig
     (F.t * ScopedTypeExpression.t) list ->
     (F.t * ScopedTypeExpression.t) list
   val merge_checked_type_abbrevs :
-    IDPosUf.t ->
+    UF.t ->
     ((IdPos.t *TypeAssignment.skema) * Loc.t) F.Map.t ->
     ((IdPos.t *TypeAssignment.skema) * Loc.t) F.Map.t ->
-    IdPos.t list * IDPosUf.t * ((IdPos.t *TypeAssignment.skema) * Loc.t) F.Map.t
+    IdPos.t list * UF.t * ((IdPos.t *TypeAssignment.skema) * Loc.t) F.Map.t
 
   val merge_toplevel_macros :
     (ScopedTerm.t * Loc.t) F.Map.t ->
@@ -1246,7 +1240,7 @@ module Flatten : sig
     let t = F.Map.union (fun f l1 l2 ->
       let to_union, ta = TypeAssignment.merge_skema f l2 l1 in
       List.iter (fun (id1,id2) ->
-        let rem, uf1 = IDPosUf.union !uf id1 id2 in
+        let rem, uf1 = UF.union !uf id1 id2 in
         uf := uf1;
         Option.iter (fun x -> to_remove := x :: !to_remove) rem;
       ) to_union;
@@ -1262,7 +1256,7 @@ module Flatten : sig
         ("Duplicate type abbreviation for " ^ F.show k ^
           ". Previous declaration: " ^ Loc.show otherloc)
       else
-        let rem, uf1 = IDPosUf.union !uf id1 id2 in
+        let rem, uf1 = UF.union !uf id1 id2 in
         uf := uf1;
         Option.iter (fun x -> to_remove := x :: !to_remove) rem;
         Some x) m1 m2 in
@@ -1335,7 +1329,7 @@ module Flatten : sig
 
   let run state { Scoped.pbody; toplevel_macros } =
     let kinds, types, type_abbrevs, clauses_rev, chr_rev = compile_body pbody in
-    let signature = { Flat.kinds; types; type_abbrevs; toplevel_macros; type_uf = IDPosUf.empty } in
+    let signature = { Flat.kinds; types; type_abbrevs; toplevel_macros; type_uf = UF.empty } in
     { Flat.clauses = List.(flatten (rev clauses_rev)); chr = List.rev chr_rev; builtins = []; signature } (* TODO builtins can be in a unit *)
 
 
@@ -1412,7 +1406,7 @@ end = struct
 
     let check_t_end = Unix.gettimeofday () in
 
-    let all_type_uf = IDPosUf.merge otuf type_uf in
+    let all_type_uf = UF.merge otuf type_uf in
     let to_remove, all_type_uf, all_types = Flatten.merge_type_assignments all_type_uf ot types in
     let all_toplevel_macros = Flatten.merge_toplevel_macros otlm toplevel_macros in
     let all_functional_preds = func_setter_object#merge in
@@ -1768,7 +1762,7 @@ let extend1_signature base_signature (signature : checked_compilation_unit_signa
   let { Assembled.kinds = ok; functional_preds = ofp; types = ot; type_abbrevs = ota; toplevel_macros = otlm; type_uf = otyuf } = base_signature in
   let { Assembled.toplevel_macros; kinds; types; type_abbrevs; functional_preds; type_uf } = signature in
   let kinds = Flatten.merge_kinds ok kinds in
-  let type_uf = IDPosUf.merge otyuf type_uf in
+  let type_uf = UF.merge otyuf type_uf in
   let to_remove, type_uf, type_abbrevs = Flatten.merge_checked_type_abbrevs type_uf ota type_abbrevs in
   let to_remove1, type_uf, types = Flatten.merge_type_assignments type_uf ot types in
   let toplevel_macros = Flatten.merge_toplevel_macros otlm toplevel_macros in

src/compiler/compiler_data.ml

@@ -4,6 +4,7 @@ open Elpi_runtime
 open Util
 module F = Ast.Func
 
+(* Globally unique identifier for symbols with a quotient *)
 module IdPos : sig 
   type t [@@deriving show,ord]
   module Map : Map.S with type key = t
@@ -12,8 +13,7 @@ module IdPos : sig
 
   val make_loc : Loc.t -> t
   val make_str : string -> t
-  val equal : t -> t -> bool
-  val hash : t -> int
+  val equal : UF.t -> t -> t -> bool
   val to_loc : t -> Loc.t
 end = struct
   include Loc
@@ -22,8 +22,7 @@ end = struct
   module UF = Union_find.Make(Map)
   let make_loc loc = loc
   let make_str str = make_loc (Loc.initial str)
-  let equal x y = compare x y = 0
-  let hash t = Hashtbl.hash t
+  let equal u x y = compare (UF.find u x) (UF.find u y) = 0
   let to_loc x = x 
 end
 
@@ -140,7 +139,7 @@ module ScopedTypeExpression = struct
     let show_var = function Ast.Structured.Variadic -> ".." | _ -> "" in
     match r.it with
     | Prop _ -> fprintf fmt "."
-    | _  -> fprintf fmt "%a:%a %s->@ %a" Mode.pp_short m pretty_e_loc l (show_var v) pretty_e_loc r
+    | _  -> fprintf fmt "%a %s->@ %a" (*Mode.pretty m*) pretty_e_loc l (show_var v) pretty_e_loc r
   and pretty_e_parens ~lvl fmt = function
     | t when lvl >= lvl_of t.it -> fprintf fmt "(%a)" pretty_e_loc t
     | t -> pretty_e_loc fmt t
@@ -351,12 +350,12 @@ module TypeAssignment = struct
 
     let rec pretty fmt = function
       | Prop Relation -> fprintf fmt "prop"
-      | Prop Function -> fprintf fmt "fprop"
+      | Prop Function -> fprintf fmt "func"
       | Any -> fprintf fmt "any"
       | Cons c -> F.pp fmt c
       | App(f,x,xs) -> fprintf fmt "@[<hov 2>%a@ %a@]" F.pp f (Util.pplist (pretty_parens ~lvl:app) " ") (x::xs)
-      | Arr(m,NotVariadic,s,t) -> fprintf fmt "@[<hov 2>%a:%a ->@ %a@]" Mode.pp_short m (pretty_parens ~lvl:arrs) s pretty t
-      | Arr(m,Variadic,s,t) -> fprintf fmt "%a:%a ..-> %a" Mode.pp_short m (pretty_parens ~lvl:arrs) s pretty t
+      | Arr(m,NotVariadic,s,t) -> fprintf fmt "@[<hov 2>(*%a:*)%a ->@ %a@]" Mode.pretty m (pretty_parens ~lvl:arrs) s pretty t
+      | Arr(m,Variadic,s,t) -> fprintf fmt "(*%a:*)%a ..-> %a" Mode.pretty m (pretty_parens ~lvl:arrs) s pretty t
       | UVar m -> f fmt pretty m
       (* | UVar m -> MutableOnce.pretty fmt m *)
     and pretty_parens ~lvl fmt = function

src/compiler/determinacy_checker.ml

@@ -5,7 +5,7 @@ open Elpi_util.Util
 open Elpi_parser.Ast
 open Compiler_data
 module C = Constants
-module Union_find = Union_find.Make (IdPos.Map)
+module UF = IdPos.UF
 
 let to_print f = if false then f ()
 
@@ -38,7 +38,7 @@ let rec pp_functionality fmt = function
   | AssumedFunctional -> Format.fprintf fmt "AF"
   | Any -> Format.fprintf fmt "Any"
   | BoundVar b -> Format.fprintf fmt "BV %a" F.pp b
-  | Arrow (m, a, b) -> Format.fprintf fmt "(%a:%a -> %a)" Mode.pp_short m pp_functionality a pp_functionality b
+  | Arrow (m, a, b) -> Format.fprintf fmt "(%a:%a -> %a)" Mode.pretty m pp_functionality a pp_functionality b
   | NoProp l -> Format.fprintf fmt "Kind [@[%a@]]" (pplist pp_functionality ",") l
 
 let get_NoProp_list ~loc = function
@@ -53,7 +53,7 @@ type env = t (* This is for the cleaner signatures in this files for objects wit
 let compare_functionality_loc a b = compare_functionality_abs (snd a) (snd b)
 let compare_fname a b = compare_functionality_loc (snd a) (snd b)
 let mk_func_map ty_abbr cmap = { ty_abbr; cmap }
-let empty_fmap = { ty_abbr = F.Map.empty; cmap = IdPos.Map.empty }
+let empty = { ty_abbr = F.Map.empty; cmap = IdPos.Map.empty }
 let get_functionality_tabbr_opt map k = F.Map.find_opt k map.ty_abbr
 
 let rec get_namef = function
@@ -196,7 +196,7 @@ let remove t k = { t with cmap = IdPos.Map.remove k t.cmap }
 let get_functionality ~uf ?tyag ~loc ~env id =
   if id = Scope.dummy_type_decl_id then Any
   else
-    let id' = Union_find.find uf id in
+    let id' = UF.find uf id in
     if id <> id' then assert (not (IdPos.Map.mem id env.cmap));
     (* Sanity check *)
     match IdPos.Map.find_opt id' env.cmap with
@@ -321,7 +321,7 @@ let not_functional_call_error ~loc t =
   error ~loc (Format.asprintf "Non functional premise call %a\n" ScopedTerm.pretty_ t)
 
 module Checker_clause = struct
-  let check ?(uf = Union_find.empty) ~(global : env) tm =
+  let check ?(uf = UF.empty) ~(global : env) tm =
     let env = ref Env.empty in
     let pp_env fmt () : unit = Format.fprintf fmt "Env : %a" Env.pp !env in
     (* let pp_ctx fmt ctx : unit = Format.fprintf fmt "Ctx : %a" Ctx.pp ctx in *)
@@ -803,7 +803,7 @@ let check_clause ?uf ~loc ~env t =
 class merger (all_func : env) =
   object (self)
     val mutable all_func = all_func
-    val mutable local_func = empty_fmap
+    val mutable local_func = empty
 
     method private add_func is_ty_abbr id ty =
       let loc, func = Compilation.ScopeTE.type2func all_func ty in

src/compiler/determinacy_checker.mli

@@ -3,15 +3,15 @@
 (* ------------------------------------------------------------------------- *)
 open Compiler_data
 open Elpi_util.Util
-module Union_find : Union_find.S with type key = IdPos.t and type t = IdPos.t IdPos.Map.t
 
 type t [@@deriving show, ord]
 
-val empty_fmap : t
-val check_clause : ?uf:Union_find.t -> loc:Loc.t -> env:t -> ScopedTerm.t -> unit
+val empty : t
 val merge : t -> t -> t
 val remove : t -> IdPos.t -> t
 
+val check_clause : ?uf:IdPos.UF.t -> loc:Loc.t -> env:t -> ScopedTerm.t -> unit
+
 class merger : t -> object
   method get_all_func : t
   method get_local_func : t

src/compiler/test_compiler_data.ml

@@ -27,15 +27,24 @@ let list x = (App(F.from_string "list",x,[]))
 let int = Cons (F.from_string "int")
 let arr s t = Arr(Output,NotVariadic,s,t)
 
-let () = pp_ta (Prop Relation) "prop";;
+(* let () = pp_ta (Prop Relation) "prop";;
 let () = pp_ta (Prop Function) "fprop";;
 let () = pp_ta (list int) "list int";;
 let () = pp_ta (list (list int)) "list (list int)";;
 let () = pp_ta (arr (list int) int) "o:list int -> int";;
 let () = pp_ta (arr (arr int int) int) "o:(o:int -> int) -> int";;
 let () = pp_ta (arr int (arr int int)) "o:int -> o:int -> int";;
 let () = pp_ta (arr int (arr (list int) int)) "o:int -> o:list int -> int";;
-let () = pp_ta (list (arr int int)) "list (o:int -> int)";;
+let () = pp_ta (list (arr int int)) "list (o:int -> int)";; *)
+let () = pp_ta (Prop Relation) "prop";;
+let () = pp_ta (Prop Function) "prop";;
+let () = pp_ta (list int) "list int";;
+let () = pp_ta (list (list int)) "list (list int)";;
+let () = pp_ta (arr (list int) int) "list int -> int";;
+let () = pp_ta (arr (arr int int) int) "(int -> int) -> int";;
+let () = pp_ta (arr int (arr int int)) "int -> int -> int";;
+let () = pp_ta (arr int (arr (list int) int)) "int -> list int -> int";;
+let () = pp_ta (list (arr int int)) "list (int -> int)";;
 
 open ScopedTerm