fixed bug in coercion application, input/output swapped in unification

[helm.git] / helm / software / components / acic_content / cicNotationUtil.ml

diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml
index 1ddd5c9c3b1572c74034fb70b4f2563867ee6786..0c8abce504694b5053f62a9feeb997c0bc6a1a4f 100644 (file)
--- a/helm/software/components/acic_content/cicNotationUtil.ml
+++ b/helm/software/components/acic_content/cicNotationUtil.ml
@@ -62,7 +62,8 @@ let visit_ast ?(special_k = fun _ -> assert false)
       | Ast.Magic _
       | Ast.Variable _) as t -> special_k t
     | (Ast.Ident _
-      | Ast.Implicit
+      | Ast.NRef _
+      | Ast.Implicit _
       | Ast.Num _
       | Ast.Sort _
       | Ast.Symbol _
@@ -99,6 +100,7 @@ let visit_layout k = function
   | Ast.Group terms -> Ast.Group (List.map k terms)
   | Ast.Mstyle (l, term) -> Ast.Mstyle (l, List.map k term)
   | Ast.Mpadded (l, term) -> Ast.Mpadded (l, List.map k term)
+  | Ast.Maction terms -> Ast.Maction (List.map k terms)
 
 let visit_magic k = function
   | Ast.List0 (t, l) -> Ast.List0 (k t, l)
@@ -206,7 +208,7 @@ let meta_names_of_term term =
     | Ast.Ident (_, Some substs) -> aux_substs substs
     | Ast.Meta (_, substs) -> aux_meta_substs substs
 
-    | Ast.Implicit
+    | Ast.Implicit _
     | Ast.Ident _
     | Ast.Num _
     | Ast.Sort _
@@ -325,13 +327,21 @@ let dressn ~sep:sauces =
 let find_appl_pattern_uris ap =
   let rec aux acc =
     function
-    | Ast.UriPattern uri -> uri :: acc
+    | Ast.UriPattern uri -> `Uri uri :: acc
+    | Ast.NRefPattern nref -> `NRef nref :: acc
     | Ast.ImplicitPattern
     | Ast.VarPattern _ -> acc
     | Ast.ApplPattern apl -> List.fold_left aux acc apl
   in
   let uris = aux [] ap in
-  HExtlib.list_uniq (List.fast_sort UriManager.compare uris)
+  let cmp u1 u2 =
+   match u1,u2 with
+      `Uri u1, `Uri u2 -> UriManager.compare u1 u2
+    | `NRef r1, `NRef r2 -> NReference.compare r1 r2
+    | `Uri _,`NRef _ -> -1
+    | `NRef _, `Uri _ -> 1
+  in
+  HExtlib.list_uniq (List.fast_sort cmp uris)
 
 let rec find_branch =
   function
@@ -361,7 +371,8 @@ let fresh_id () =
   !fresh_index
 
   (* TODO ensure that names generated by fresh_var do not clash with user's *)
-let fresh_name () = "η" ^ string_of_int (fresh_id ())
+  (* FG: "η" is not an identifier (it is rendered, but not be parsed) *)
+let fresh_name () = "eta" ^ string_of_int (fresh_id ())
 
 let rec freshen_term ?(index = ref 0) term =
   let freshen_term = freshen_term ~index in
@@ -395,11 +406,11 @@ let freshen_obj obj =
           indtypes
       in
       CicNotationPt.Inductive (freshen_capture_variables params, indtypes)
-  | CicNotationPt.Theorem (flav, n, t, ty_opt) ->
+  | CicNotationPt.Theorem (flav, n, t, ty_opt,p) ->
       let ty_opt =
         match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
       in
-      CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt)
+      CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt,p)
   | CicNotationPt.Record (params, n, ty, fields) ->
       CicNotationPt.Record (freshen_capture_variables params, n,
         freshen_term ty, freshen_name_ty_b fields)