[compiler] modes in SymbolMap + macro clone

- remove modes from program
- modes are deduced from types
- modes are added to the symbol map during the creation of the indexing

- add clone function for terms, this is needed since terms contains
  pointers: memory sharing cannot be performed

- macro are cloned before doing beta reduction
  this avoids type assignments to be wrongly assigned by side effects
  (add test for this: see macro_type.elpi)

- typechecker does not perform typechecking if the ty projection of a
  ScopedTerm has been already set (this means that the term has already
  been typechecked)


- pretty printer of scoped term takes a function printing values
  carried by Uvar (Uvar carries a polymorphic object)

src/compiler/compiler_data.ml

@@ -14,6 +14,7 @@ module IdPos : sig
   val make_str : string -> t
   val equal : t -> t -> bool
   val hash : t -> int
+  val to_loc : t -> Loc.t
 end = struct
   include Loc
   module Map = Map.Make(Loc)
@@ -23,6 +24,7 @@ end = struct
   let make_str str = make_loc (Loc.initial str)
   let equal x y = compare x y = 0
   let hash t = Hashtbl.hash t
+  let to_loc x = x 
 end
 
 module Scope = struct
@@ -44,6 +46,8 @@ module Scope = struct
       }
   [@@ deriving show, ord]
 
+  let clone = function Bound _ as t -> t | Global {escape_ns; decl_id} -> Global {escape_ns; decl_id}
+
   module Map = Map.Make(struct
     type t = F.t * language
     [@@ deriving show, ord]
@@ -220,7 +224,7 @@ module MutableOnce : sig
   [@@ deriving show]
   val make : F.t -> 'a t
   val create : 'a -> 'a t
-  val set : 'a t -> 'a -> unit
+  val set : ?loc:Loc.t -> 'a t -> 'a -> unit
   val unset : 'a t -> unit
   val get : 'a t -> 'a
   val get_name : 'a t -> F.t
@@ -235,10 +239,10 @@ end = struct
   let create t = F.from_string "_", ref (Some t)
 
   let is_set (_,x) = Option.is_some !x
-  let set (_,r) x =
+  let set ?loc (_,r) x =
     match !r with
     | None -> r := Some x
-    | Some _ -> anomaly "MutableOnce"
+    | Some _ -> anomaly ?loc "MutableOnce"
 
   let get (_,x) = match !x with Some x -> x | None -> anomaly "get"
   let get_name (x,_) = x
@@ -266,6 +270,38 @@ module TypeAssignment = struct
     | UVar of 'a
   [@@ deriving show, fold, ord]
 
+  exception InvalidMode
+
+  let cmp_aux cmp1 k =
+    if cmp1 = 0 then k () else cmp1
+
+  let rec compare_t_ c t1 t2 = match t1, t2 with
+    | Prop _, Prop _ -> 0
+    | Any, Any -> 0
+    | Cons f1, Cons f2 -> F.compare f1 f2
+    | App (f1,hd,tl), App (f2,hd1,tl1) -> 
+      cmp_aux 
+        (F.compare f1 f2)
+        (fun () -> List.compare (compare_t_ c) (hd::tl) (hd1::tl1))
+    | Arr (m1, v1, l1, r1), Arr (m2, v2, l2, r2) when m1 <> m2 ->
+      cmp_aux
+        (Ast.Structured.compare_variadic v1 v2) (fun () -> 
+          cmp_aux (compare_t_ c l1 l2) (fun () -> 
+            let cmp2 = compare_t_ c r1 r2 in
+            if cmp2 = 0 then raise InvalidMode
+            else cmp2))
+    | Arr (_, v1, l1, r1), Arr (_, v2, l2, r2) ->
+      cmp_aux
+        (Ast.Structured.compare_variadic v1 v2) (fun () -> 
+          cmp_aux (compare_t_ c l1 l2) (fun () -> 
+            compare_t_ c r1 r2))
+    | UVar v1, UVar v2 -> c v1 v2
+    | Prop _, _ -> -1 | _, Prop _ -> 1
+    | Any   , _ -> -1 | _, Any    -> 1
+    | Cons _, _ -> -1 | _, Cons _ -> 1
+    | App _ , _ -> -1 | _, App _  -> 1
+    | Arr _ , _ -> -1 | _, Arr _  -> 1
+
   type skema = Lam of F.t * skema | Ty of F.t t_
   [@@ deriving show, ord]
   type overloaded_skema = skema overloading
@@ -279,6 +315,8 @@ module TypeAssignment = struct
   type t = Val of t MutableOnce.t t_
   [@@ deriving show]
 
+  let new_ty () : t MutableOnce.t = MutableOnce.make (F.from_string "Ty")
+
   let nparams (_,t : skema_w_id) =
       let rec aux = function Ty _ -> 0 | Lam(_,t) -> 1 + aux t in
       aux t
@@ -311,30 +349,37 @@ module TypeAssignment = struct
 
   let apply (_,sk:skema_w_id) args = apply F.Map.empty sk args
 
-  let eq_skema_w_id (_,x) (_,y) = compare_skema x y = 0
-  let diff_id_check ((id1:IdPos.t),_) (id2,_) = assert (id1<>id2)
-  let diff_ids_check e = List.iter (diff_id_check e)
+  let eq_skema_w_id n (loc1,x) (loc2,y) = 
+    try compare_skema x y = 0
+    with InvalidMode -> 
+      error ~loc:(IdPos.to_loc loc1) 
+        (Format.asprintf "duplicate mode declaration for %a (second mode found at %a)\nDebug:\n-@[<hov 2>%a@]\n-@[<hov 2>%a@]" F.pp n IdPos.pp loc2 pp_skema x pp_skema y)
 
   (* returns a pair of ids representing the merged type_ass + the new merge type_ass *)
-  let merge_skema t1 t2 =
+  let merge_skema n t1 t2 =
+    let diff_id_check ((id1:IdPos.t),t1) (id2,t2) = 
+      if (id1 = id2) then error ~loc:(IdPos.to_loc id1) 
+        (Format.asprintf "Different constants with same ids (loc2 is:%a)\n%a\n<>\n%a" IdPos.pp id2 pp_skema t1 pp_skema t2) in
+    let diff_ids_check e = List.iter (diff_id_check e) in
+
     let removed = ref [] in
     let add x y = removed := (fst x,fst y) :: !removed in 
     let rec remove_mem e acc = function
       | [] -> List.rev acc
-      | x::xs when eq_skema_w_id e x ->
+      | x::xs when eq_skema_w_id n e x ->
         diff_ids_check x xs;
         add x e;
         List.rev_append acc xs
       | x::xs -> remove_mem e (x::acc) xs
     in
     let rec merge_aux t1 t2 =
       match t1, t2 with
-      | Single x, Single y when eq_skema_w_id x y -> 
+      | Single x, Single y when eq_skema_w_id n x y -> 
         add y x;
         t1
       | Single x, Single y -> diff_id_check x y; Overloaded [x;y]
       | Single x, Overloaded ys  -> Overloaded (x :: remove_mem x [] ys)
-      | Overloaded xs, Single y when List.exists (eq_skema_w_id y) xs -> t1
+      | Overloaded xs, Single y when List.exists (eq_skema_w_id n y) xs -> t1
       | Overloaded xs, Single y -> diff_ids_check y xs; Overloaded(xs@[y])
       | Overloaded xs, Overloaded _ ->
           List.fold_right (fun x -> merge_aux (Single x)) xs t2
@@ -379,7 +424,7 @@ module TypeAssignment = struct
     | Overloaded l -> List.exists (fun (_,x) -> is_predicate x) l
 
   open Format
-  let pretty fmt tm =
+  let pretty f fmt tm =
 
     let arrs = 0 in
     let app = 1 in
@@ -397,16 +442,33 @@ module TypeAssignment = struct
       | 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
-      | UVar m when MutableOnce.is_set m -> pretty fmt @@ deref m
-      | UVar m -> MutableOnce.pretty fmt m
+      | UVar m -> f fmt pretty m
+      (* | UVar m -> MutableOnce.pretty fmt m *)
     and pretty_parens ~lvl fmt = function
-      | UVar m when MutableOnce.is_set m -> pretty_parens ~lvl fmt @@ deref m
+      | UVar m -> f fmt (pretty_parens ~lvl) m
       | t when lvl >= lvl_of t -> fprintf fmt "(%a)" pretty t
       | t -> pretty fmt t in
     let pretty fmt t = Format.fprintf fmt "@[%a@]" pretty t
   in 
   pretty fmt tm
 
+  let pretty_mut_once = 
+    pretty (fun fmt f t -> if MutableOnce.is_set t then f fmt (deref t) else MutableOnce.pretty fmt t)
+
+  let pretty_ft =
+    pretty (fun fmt _ (t:F.t) -> F.pp fmt t)
+
+  let pretty_skema_w_id fmt ((_, sk):skema_w_id) =
+    let rec aux = function
+      | Lam (_,t) -> aux t
+      | Ty t -> pretty_ft fmt t in
+    aux sk
+
+  let pretty_overloaded_skema fmt = function
+    | Single t -> pretty_skema_w_id fmt t
+    | Overloaded l -> pplist pretty_skema_w_id "," fmt l
+
+
   let vars_of (Val t)  = fold_t_ (fun xs x -> if MutableOnce.is_set x then xs else x :: xs) [] t
 
 end
@@ -511,7 +573,7 @@ module ScopedTerm = struct
   let build_infix_constant scope name loc : t = {loc; ty = MutableOnce.make (F.from_string "dummy"); it = Const (scope, name)}
 
   let is_infix_constant f =
-    let infix = [F.andf; F.orf; F.eqf; F.isf; F.asf; F.consf] in
+    let infix = [F.andf; F.orf; F.eqf; F.isf; F.asf; F.consf; F.from_string "^"] in
     List.mem f infix
 
   let intersperse e : 'a -> t list = function
@@ -521,7 +583,7 @@ module ScopedTerm = struct
   let rec pretty_lam fmt n ste (mta:TypeAssignment.t MutableOnce.t) it =
     fprintf fmt "%a" F.pp (get_lam_name n);
     if MutableOnce.is_set mta then
-      fprintf fmt ": %a " TypeAssignment.pretty (match MutableOnce.get mta with Val a -> a)
+      fprintf fmt ": %a " TypeAssignment.pretty_mut_once (match MutableOnce.get mta with Val a -> a)
     else Option.iter (fun e -> fprintf fmt ": %a " ScopedTypeExpression.pretty_e e) ste;
     fprintf fmt "\\ %a" pretty it;
 
@@ -623,6 +685,18 @@ module ScopedTerm = struct
       | Discard | CData _ -> t
     and rename_loc l c d { it; ty; loc } = { it = rename l c d it; ty; loc } 
 
+    let rec clone_loc {it;loc} = {it=clone it;loc;ty=TypeAssignment.new_ty ()} and
+    clone = function
+      | Const (g, x) -> Const (Scope.clone g, x)
+      | Impl (b, l, r) -> Impl(b, clone_loc l, clone_loc r)
+      | Lam (n,ty,_,bo) -> Lam(n,ty,TypeAssignment.new_ty (), clone_loc bo)
+      | Discard -> Discard
+      | Var (v, xs) -> Var (v, List.map clone_loc xs)
+      | App (g, n, x, xs) -> App (Scope.clone g, n, clone_loc x, List.map clone_loc xs)
+      | CData _ as t -> t 
+      | Spill (t, _) -> Spill (clone_loc t, ref NoInfo)
+      | Cast (t, ty) -> Cast (clone_loc t, ty)
+
     let beta t args =
       let rec fv acc { it } =
         match it with
@@ -653,7 +727,7 @@ module ScopedTerm = struct
             let d = fresh () in
             Lam(Some (d,l),ty,tya,subst_loc map fv @@ rename_loc l c d t)
         | Const(Bound l,c) when Scope.Map.mem (c,l) map -> unlock @@ Scope.Map.find (c,l) map
-        | Const _ -> t
+        | Const (x,y) -> Const (x, y)
         | App(Bound l,c,x,xs) when Scope.Map.mem (c,l) map ->
             let hd = Scope.Map.find (c,l) map in
             unlock @@ app_loc hd (List.map (subst_loc map fv) (x::xs))
@@ -662,8 +736,8 @@ module ScopedTerm = struct
         | Spill(t,i) -> Spill(subst_loc map fv t,i)
         | Cast(t,ty) -> Cast(subst_loc map fv t,ty)
         | Discard | CData _ -> t
-      and subst_loc map fv { it; ty; loc } = { it = subst map fv it; ty; loc }
-      and app_loc { it; loc; ty } args : t = { it = app ~loc it args; loc; ty }
+      and subst_loc map fv { it; ty; loc } = {loc; it = (subst map fv it); ty}
+      and app_loc { it; loc; ty } args : t = {loc; it = (app ~loc it args); ty}
       and app ~loc t (args : t list) =
         if args = [] then t else
         match t with
@@ -677,6 +751,7 @@ module ScopedTerm = struct
         | Cast _ -> error ~loc "cannot apply cast"
         | Lam _ -> load_subst ~loc t args Scope.Map.empty Scope.Set.empty
       in
+        if args = [] then unlock t else
         load_subst_loc t args Scope.Map.empty Scope.Set.empty
 
   module QTerm = struct

src/compiler/test_compiler_data.ml

@@ -1,9 +1,9 @@
 let pp_ta t s =
   let open Elpi_compiler.Compiler_data in
-  let s' = Format.asprintf "@[%a@]" TypeAssignment.pretty t in
+  let s' = Format.asprintf "@[%a@]" TypeAssignment.pretty_mut_once t in
   if s <> s' then begin
     Format.eprintf "Unexpected print: %a\nactual: %a\nreference: %s\n"
-      TypeAssignment.pp (Val t) TypeAssignment.pretty t s;
+      TypeAssignment.pp (Val t) TypeAssignment.pretty_mut_once t s;
     exit 1
   end
 ;;

src/compiler/test_type_checker.ml

@@ -48,7 +48,7 @@ let _ =
     let t = get_uvar @@ TA.unval (MutableOnce.get t.ST.ty) in
     (* let pp = TA.pp_t_ (MutableOnce.pp TA.pp) in *)
     if t <> exp then (
-      Format.eprintf "Unexpected result: \nactual: @[%a@]\nreference: @[%a@]\n" TA.pretty t TA.pretty exp;
+      Format.eprintf "Unexpected result: \nactual: @[%a@]\nreference: @[%a@]\n" TA.pretty_mut_once t TA.pretty_mut_once exp;
       exit 1)
   in
 

src/compiler/type_checker.ml

@@ -90,53 +90,55 @@ type env_undeclared = (TypeAssignment.t * Scope.type_decl_id * Ast.Loc.t) F.Map.
 
 open ScopedTerm
 
+let pretty_ty = TypeAssignment.pretty_mut_once
+
 let error_not_a_function ~loc c tyc args x =
   let t =
     if args = [] then ScopedTerm.Const(Scope.mkGlobal ~escape_ns:true (),c)
     else ScopedTerm.(App(Scope.mkGlobal ~escape_ns:true (),c,List.hd args, List.tl args)) in
   let msg = Format.asprintf "@[<hov>%a is not a function but it is passed the argument@ @[<hov>%a@].@ The type of %a is %a@]"
-    ScopedTerm.pretty_ t ScopedTerm.pretty x F.pp c TypeAssignment.pretty tyc in
+    ScopedTerm.pretty_ t ScopedTerm.pretty x F.pp c TypeAssignment.pretty_mut_once tyc in
   error ~loc msg
 
 let pp_tyctx fmt = function
   | None -> Format.fprintf fmt "its context"
   | Some c -> Format.fprintf fmt "%a" F.pp c
 
 let error_bad_cdata_ety ~loc ~tyctx ~ety c tx =
-  let msg = Format.asprintf "@[<hov>literal \"%a\" has type %a@ but %a expects a term of type@ %a@]"  CData.pp c TypeAssignment.pretty tx pp_tyctx tyctx TypeAssignment.pretty ety in
+  let msg = Format.asprintf "@[<hov>literal \"%a\" has type %a@ but %a expects a term of type@ %a@]"  CData.pp c pretty_ty tx pp_tyctx tyctx pretty_ty ety in
   error ~loc msg
 
 let error_bad_ety ~loc ~tyctx ~ety pp c tx =
-  let msg = Format.asprintf "@[<hov>%a has type %a@ but %a expects a term of type@ %a@]"  pp c TypeAssignment.pretty tx pp_tyctx tyctx TypeAssignment.pretty ety in
+  let msg = Format.asprintf "@[<hov>%a has type %a@ but %a expects a term of type@ %a@]"  pp c pretty_ty tx pp_tyctx tyctx pretty_ty ety in
   error ~loc msg
 
 let error_bad_ety2 ~loc ~tyctx ~ety1 ~ety2 pp c tx =
-  let msg = Format.asprintf "@[<hov>%a has type %a@ but %a expects a term of type@ %a@ or %a@]"  pp c TypeAssignment.pretty tx pp_tyctx tyctx TypeAssignment.pretty ety1 TypeAssignment.pretty ety2 in
+  let msg = Format.asprintf "@[<hov>%a has type %a@ but %a expects a term of type@ %a@ or %a@]"  pp c pretty_ty tx pp_tyctx tyctx pretty_ty ety1 pretty_ty ety2 in
   error ~loc msg
 
 let error_bad_function_ety ~loc ~tyctx ~ety c t =
-  let msg = Format.asprintf "@[<hov>%a is a function@ but %a expects a term of type@ %a@]"  ScopedTerm.pretty_ ScopedTerm.(Lam(c,None,ScopedTerm.mk_empty_lam_type c,t)) pp_tyctx tyctx TypeAssignment.pretty ety in
+  let msg = Format.asprintf "@[<hov>%a is a function@ but %a expects a term of type@ %a@]"  ScopedTerm.pretty_ ScopedTerm.(Lam(c,None,ScopedTerm.mk_empty_lam_type c,t)) pp_tyctx tyctx pretty_ty ety in
   error ~loc msg
 
 let error_bad_const_ety_l ~loc ~tyctx ~ety c txl =
-  let msg = Format.asprintf "@[<hv>%a is overloaded but none of its types matches the type expected by %a:@,  @[<hov>%a@]@,Its types are:@,@[<v 2>  %a@]@]" F.pp c pp_tyctx tyctx TypeAssignment.pretty ety (pplist ~boxed:true (fun fmt (_,x)-> Format.fprintf fmt "%a" TypeAssignment.pretty x) ", ") txl in
+  let msg = Format.asprintf "@[<hv>%a is overloaded but none of its types matches the type expected by %a:@,  @[<hov>%a@]@,Its types are:@,@[<v 2>  %a@]@]" F.pp c pp_tyctx tyctx pretty_ty ety (pplist ~boxed:true (fun fmt (_,x)-> Format.fprintf fmt "%a" pretty_ty x) ", ") txl in
   error ~loc msg
 
 let error_overloaded_app ~loc ~ety c args alltys =
   let ty = arrow_of_args args ety in
-  let msg = Format.asprintf "@[<v>%a is overloaded but none of its types matches:@,  @[<hov>%a@]@,Its types are:@,@[<v 2>  %a@]@]" F.pp c TypeAssignment.pretty ty (pplist (fun fmt (_,x)-> Format.fprintf fmt "%a" TypeAssignment.pretty x) ", ") alltys in
+  let msg = Format.asprintf "@[<v>%a is overloaded but none of its types matches:@,  @[<hov>%a@]@,Its types are:@,@[<v 2>  %a@]@]" F.pp c pretty_ty ty (pplist (fun fmt (_,x)-> Format.fprintf fmt "%a" pretty_ty x) ", ") alltys in
   error ~loc msg
 
 let error_overloaded_app_tgt ~loc ~ety c =
-  let msg = Format.asprintf "@[<v>%a is overloaded but none of its types matches make it build a term of type @[<hov>%a@]@]" F.pp c TypeAssignment.pretty ety in
+  let msg = Format.asprintf "@[<v>%a is overloaded but none of its types matches make it build a term of type @[<hov>%a@]@]" F.pp c pretty_ty ety in
   error ~loc msg
 
 
 let error_not_poly ~loc c ty sk =
   error ~loc (Format.asprintf "@[<hv>this rule imposes on %a the type@ %a@ is less general than the declared one@ %a@]"
     F.pp c
-    TypeAssignment.pretty ty
-    TypeAssignment.pretty sk)
+    pretty_ty ty
+    pretty_ty sk)
 
 type ret = TypeAssignment.t MutableOnce.t TypeAssignment.t_
 type ret_id = IdPos.t * TypeAssignment.t MutableOnce.t TypeAssignment.t_
@@ -271,9 +273,9 @@ let check ~is_rule ~type_abbrevs ~kinds ~types:env ~unknown (t : ScopedTerm.t) ~
 
   and check_lam ctx ~loc ~tyctx c cty tya t ety =
     let name_lang = match c with Some c -> c | None -> fresh_name (), elpi_language in
-    let set_tya_ret f = MutableOnce.set tya (Val f); f in
+    let set_tya_ret f = MutableOnce.set ~loc tya (Val f); f in
     let src = set_tya_ret @@ match cty with
-      | None ->  mk_uvar "Src"
+      | None -> mk_uvar "Src"
       | Some x -> TypeAssignment.subst (fun f -> Some (UVar(MutableOnce.make f))) @@ check_loc_tye ~type_abbrevs ~kinds F.Set.empty x
     in
     let tgt = mk_uvar "Tgt" in
@@ -366,7 +368,7 @@ let check ~is_rule ~type_abbrevs ~kinds ~types:env ~unknown (t : ScopedTerm.t) ~
     | (id,t)::ts ->
         (* Format.eprintf "checking overloaded app %a\n" F.pp c; *)
         match classify_arrow t with
-        | Unknown -> error ~loc (Format.asprintf "Type too ambiguous to be assigned to the overloaded constant: %s for type %a" (F.show c) TypeAssignment.pretty t)
+        | Unknown -> error ~loc (Format.asprintf "Type too ambiguous to be assigned to the overloaded constant: %s for type %a" (F.show c) pretty_ty t)
         | Simple { srcs; tgt } ->
           (* Format.eprintf "argsty : %a\n" TypeAssignment.pretty (arrow_of_tys targs ety); *)
             if try_unify (arrow_of_tys srcs tgt) (arrow_of_tys targs ety) then (resolve_gid id cid;[]) (* TODO: here we should something ? *)
@@ -405,12 +407,12 @@ let check ~is_rule ~type_abbrevs ~kinds ~types:env ~unknown (t : ScopedTerm.t) ~
         | _ -> error_not_a_function ~loc:x.loc (fst c) ty (List.rev consumed) x (* TODO: trim loc up to x *)
 
   and check_loc ~tyctx ctx { loc; it; ty } ~ety : spilled_phantoms =
-    (* if MutableOnce.is_set ty then []
-    else *)
+    if MutableOnce.is_set ty then []
+    else
       begin
         (* assert (not @@ MutableOnce.is_set ty); *)
         let extra_spill = check ~tyctx ctx ~loc it ety in
-        if not @@ MutableOnce.is_set ty then MutableOnce.set ty (Val ety);
+        MutableOnce.set ty (Val ety);
         extra_spill
       end
 
@@ -588,10 +590,10 @@ let check ~is_rule ~type_abbrevs ~kinds ~types:env ~unknown (t : ScopedTerm.t) ~
 
 let check1_undeclared w f (t, id, loc) =
   match TypeAssignment.is_monomorphic t with
-  | None -> error ~loc Format.(asprintf "@[Unable to infer a closed type for %a:@ %a@]" F.pp f TypeAssignment.pretty (TypeAssignment.unval t))
+  | None -> error ~loc Format.(asprintf "@[Unable to infer a closed type for %a:@ %a@]" F.pp f pretty_ty (TypeAssignment.unval t))
   | Some ty ->
       if not @@ Re.Str.(string_match (regexp "^\\(.*aux[0-9']*\\|main\\)$") (F.show f) 0) then
-        w := Format.((f, loc), asprintf "type %a %a." F.pp f TypeAssignment.pretty (TypeAssignment.unval t)) :: !w;
+        w := Format.((f, loc), asprintf "type %a %a." F.pp f pretty_ty (TypeAssignment.unval t)) :: !w;
       TypeAssignment.Single (id, ty)
 
 let check_undeclared ~unknown =

src/parser/ast.ml

@@ -30,6 +30,7 @@ module Func = struct
   let show x = x
   let equal x y = x == y || x = y (* Resilient to unmarshaling *)
   let truef = from_string "true"
+  let discardf = from_string "_"
   let andf = from_string ","
   let orf = from_string ";"
   let implf = from_string "=>"