qname keyword

src/builtin.elpi

@@ -50,6 +50,8 @@ external symbol (,)   : variadic (func) (func).
 
 external symbol uvar  : A = "core".
 
+external symbol qname : A = "core".
+
 external symbol (as)  : A -> A -> A = "core".
 
 external symbol (=>)  : (pred) -> (func) -> (func) = "core".

src/builtin.ml

@@ -244,6 +244,7 @@ external func pattern_match A -> A.|};
   LPCode "external symbol (:-)  : (func) -> list (pred) -> (func) = \"core\".";
   LPCode "external symbol (,)   : variadic (func) (func).";
   LPCode "external symbol uvar  : A = \"core\".";
+  LPCode "external symbol qname : A = \"core\".";
   LPCode "external symbol (as)  : A -> A -> A = \"core\".";
   LPCode "external symbol (=>)  : (pred) -> (func) -> (func) = \"core\".";
   LPCode "external symbol (=>)  : list (pred) -> (func) -> (func) = \"core\"."; (* HACK in TC to handle this*)

src/compiler/compiler.ml

@@ -1801,6 +1801,7 @@ end = struct
     (!symb, !amap), t
 
   let check_mut_excl state symbols ~loc pred_info cl cl_st (oc: overlap_clause option) p amap : pred_info C.Map.t =
+    (* Printf.printf "Checking %s\n ov_l %s\n" (Loc.show loc) (match oc with Some {overlap_loc} -> (match overlap_loc with | Some x -> Loc.show x | _ -> "Some") | _ -> "None"); *)
     let pp_global_predicate fmt p =
       let f = SymbolMap.global_name state symbols p in
       Format.fprintf fmt "predicate %a" F.pp f in
@@ -1904,9 +1905,13 @@ end = struct
       b
     in *)
     let is_eigen_variable ~min_depth ~depth = function
-      | Const b -> min_depth <= b && b < depth
+      | (Const k | App(k,_,_)) -> (min_depth <= k && k < depth)
       | _ -> false
     in
+    let is_qname = function
+    | (Const k | App(k,_,_)) -> k == Global_symbols.namec
+    | _ -> false
+    in
     let rec is_unif_var = function
       | AppUVar _ | UVar (_, _) | Discard | Arg (_, _)|AppArg (_, _) -> true
       | App (h,x,xs) when h == Global_symbols.asc -> is_unif_var x && List.for_all is_unif_var xs
@@ -1924,8 +1929,10 @@ end = struct
       let rig_occ = ref true in
       let has_input = ref false in
       let is_catchall = ref true in
+      let has_qname = ref false in
       let update_bools m t =
         has_input := !has_input || m;
+        has_qname := !has_qname || is_qname t;
         rig_occ := !rig_occ && (is_eigen_variable ~min_depth ~depth t);
         is_catchall := !is_catchall && is_unif_var t
       in
@@ -1942,39 +1949,47 @@ end = struct
         | (([] as is) | (_::is)), _::args, [] -> mkDiscard :: mkpats is args mode
         | _ -> assert false
       in
-      (not !has_input || !rig_occ), (not !has_input || !is_catchall), R.mkAppL p @@ mkpats indexed_args args mode 
+      (not !has_input || !rig_occ), (not !has_input || !is_catchall), (!has_input && !has_qname), R.mkAppL p @@ mkpats indexed_args args mode 
     in
 
-    (* Returns if the clause has a bang *)
     let check_overlaps ~is_local ~loc ~min_depth ~depth (cl:clause) h (cl_overlap:overlap_clause option) p args (index : int * pred_info) =
       match cl_overlap with
         | None -> ()
         | Some cl_overlap ->
-          let rec filter_overlaps (arg_nb:int) has_cut : overlap_clause list -> 'a list = function
-            | [] -> []
-            | x::xs when x.timestamp = cl.timestamp -> if x.has_cut then [] else filter_overlaps arg_nb has_cut xs
+          (* arg_nb is for variadic implementataions *)
+          let rec filter_overlaps arg_nb : overlap_clause list -> 'a list = function
+            | [] -> anomaly ~loc "clause should be in the filtered list"
+            (* we find the current clause --> if it has a cut, then it discards xs else xs are kept as alternatives *)
+            | x::xs when x.timestamp = cl.timestamp ->
+              if x.has_cut then [] else xs
+            (* x has higher prio then cl, then if it has a cut, then does not overlap with cl, otherwise yes *)
             | x::xs ->
-              if not x.has_cut && arg_nb = x.arg_nb then (x::filter_overlaps arg_nb has_cut xs)
-              else filter_overlaps arg_nb has_cut xs
+              let tl = filter_overlaps arg_nb xs in
+              if x.has_cut || x.arg_nb <> arg_nb then tl else x :: tl
           in
-          let all_input_eigen_vars, all_input_catchall, hd = hd_query ~loc ~min_depth ~depth p args in
+          let all_input_eigen_vars, all_input_catchall, has_qname, hd = hd_query ~loc ~min_depth ~depth p args in
           (* Format.eprintf "Is_local:%b -- Has bang? %b -- rig_occ:%b -- is_chatchall:%b@." is_local cl_overlap.has_cut has_input_w_eigen_var is_catchall; *)
-          if is_local && not cl_overlap.has_cut && not all_input_eigen_vars then (
-            error_overlapping_eigen_variables ~loc p h);
-          if not is_local && all_input_catchall then
+          if is_local && not cl_overlap.has_cut then (
+            if all_input_eigen_vars then 
+              (* Here we have a local clause with all input vars being eigenvars + the has no cut in the body, we add the info to the pred *)
+              add_pred_w_eigen_var_no_cut p loc
+            else error_overlapping_eigen_variables ~loc p h);
+          if (not is_local && all_input_catchall) || has_qname then
             (* We check if there is a local clause for p loading a local clause without cut, if this is the case,
                we throw an error, the catchall make $p$ non functional *)
             (match get_opt p with
             | None | Some {has_local_without_cut = None} -> ()
             | Some {has_local_without_cut = (Some _) as loc1} ->
               error_overlapping ~is_local ~loc p [{ overlap_loc = loc1; timestamp =[]; has_cut = false; arg_nb = 0 }] h);
-          if is_local && not cl_overlap.has_cut && all_input_eigen_vars then
-            (* Here we have a local clause with all input vars being eigenvars + the has no cut in the body, we add the info to the pred *)
-            add_pred_w_eigen_var_no_cut p loc;
           if not is_local || (is_local && not cl_overlap.has_cut) then
+            (
+              (* Format.printf "==============================================================================================\n"; *)
+            (* Format.printf "Qui checking %a\n" pp_overlap_clause cl_overlap; *)
             let all_overlapping = get_overlapping index p hd in
-            let overlapping =  filter_overlaps cl_overlap.arg_nb cl_overlap.has_cut all_overlapping in
-            if overlapping <> [] then error_overlapping ~loc ~is_local p overlapping h
+            (* Format.printf "Overlapping list is %a\n" (pplist pp_overlap_clause "\n\t\t\t") all_overlapping; *)
+            let overlapping =  filter_overlaps cl_overlap.arg_nb all_overlapping in
+            (* Format.printf "Overlapping list is %a" (pplist pp_overlap_clause "\n\t\t\t") overlapping; *)
+            if overlapping <> [] then error_overlapping ~loc ~is_local p overlapping h)
     in
 
     (* Inspect the a local premise. If a local clause is found
@@ -2025,8 +2040,8 @@ end = struct
 (* state symbols ~loc pred_info cl body overlap_clause p amap *)
     check_clause ~min_depth:0 ~loc ~is_local:false ~lcs:0 ~depth:0 pred_info cl cl_st oc p amap;
     let pred_info = C.Map.fold (fun k v -> C.Map.add k {(C.Map.find k pred_info) with has_local_without_cut = Some v}) !preds_w_eigen_var_no_cut pred_info in
+    (* Format.eprintf "The predicates with local clauses are :@ @[%a@]@." (C.Map.pp (Loc.pp)) !preds_w_eigen_var_no_cut; *)
     pred_info 
-    (* Format.eprintf "The predicates with local clauses bla is :@ @[%a@]@." (C.Map.pp (Loc.pp)) !preds_w_eigen_var_no_cut *)
 
   let spill_todbl ?(ctx=Scope.Map.empty) ~builtins ~needs_spilling ~type_abbrevs ~types state symb ?(depth=0) ?(amap = F.Map.empty) t =
     let t = if needs_spilling then Spilling.main ~types ~type_abbrevs t else t in

src/runtime/data.ml

@@ -527,8 +527,9 @@ end
 
 let elpi_state_descriptor = State.new_descriptor ()
 
-type core_symbol = As | Uv | ECons | ENil [@@deriving enum, ord, show]
+type core_symbol = Name | As | Uv | ECons | ENil [@@deriving enum, ord, show]
 let func_of_core_symbol = function
+  | Name  -> F.from_string "qname"
   | As    -> F.asf
   | Uv    -> F.from_string "uvar"
   | ECons  -> F.consf
@@ -746,13 +747,15 @@ module Global_symbols : sig
   val delay : symbol
 
   (* core symbols *)
+  val name : symbol
   val as_      : symbol
   val uvar    : symbol
   val nil    : symbol
   val cons    : symbol
 
   (* internal *)
   val uvarc : constant (* needed by runtime/unif *)
+  val namec : constant (* needed by runtime/unif *)
   val asc : constant (* needed by runtime/unif *)
   val orc      : constant (* needed by coq-elpi *)
   val nilc     : constant (* needed by indexing *)
@@ -803,6 +806,7 @@ let uvarc, uvar = declare_core_symbol Uv
 let asc, as_ = declare_core_symbol As
 let nilc, nil = declare_core_symbol ENil
 let consc, cons = declare_core_symbol ECons
+let namec, name = declare_core_symbol Name
 
 let declare_overloaded_global_symbol str =
   let symb, variant = Symbol.make_variant_builtin (Ast.Func.from_string str) in
@@ -1438,7 +1442,7 @@ let do_allocate_constructors ty l =
   if StrSet.cardinal names <> List.length l then
     anomaly ("Duplicate constructors name in ADT: " ^ Conversion.show_ty_ast ty);
   List.fold_left (fun vacc (K(name,_,a,b,m)) ->
-    if name = "uvar" then
+    if name = "uvar" || name = "qname" then
       vacc
     else
       let c_variant = Global_symbols.declare_overloaded_global_symbol name in
@@ -1451,6 +1455,10 @@ let compile_constructors allocated ty self self_name l =
       let args = compile_arguments a self in
       let acc = Constants.Map.add Global_symbols.uvarc (XK(args,compile_builder a b,compile_matcher a m)) acc in
       (acc, sacc)
+    else if name = "qname" then
+      let args = compile_arguments a self in
+      let acc = Constants.Map.add Global_symbols.namec (XK(args,compile_builder a b,compile_matcher a m)) acc in
+      (acc, sacc)
     else
       let c =
         try StrMap.find name allocated |> fst
@@ -1477,7 +1485,7 @@ let document_adt doc ty ks cks vks fmt () =
     begin pp_comment fmt ("% " ^ doc); Fmt.fprintf fmt "@\n" end;
   document_kind fmt ty;
   List.iter (fun (K(name,doc,_,_,_)) ->
-    if name <> "uvar" then
+    if name <> "uvar" && name <> "qname" then
       let argsdoc = StrMap.find name cks in
       document_constructor fmt name (StrMap.find name vks |> snd) doc argsdoc) ks