First commit with new (incomplete) disambiguation engine.

[helm.git] / matitaB / components / content / notationPp.ml

diff --git a/matitaB/components/content/notationPp.ml b/matitaB/components/content/notationPp.ml
index 8828a03216bb74c64b71db833276fdd8c500d662..99255465d0fdcff99268d365ad64e274adac50b7 100644 (file)
--- a/matitaB/components/content/notationPp.ml
+++ b/matitaB/components/content/notationPp.ml
@@ -79,6 +79,12 @@ let pp_capture_variable pp_term =
   | term, Some typ -> "(" ^ pp_term (* ~pp_parens:false *) term ^ ": " ^ pp_term typ ^ ")"
 
 let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
+  let pp_ident = function
+  | Ast.Ident (id,`Ambiguous) -> "A:" ^ id
+  | Ast.Ident (id,`Rel) -> "R:" ^ id
+  | Ast.Ident (id,`Uri u) -> ("U:(" ^ id ^ "," ^ u ^ ")")
+  | _ -> "E"
+  in
   let pp_term = pp_term status in
   let t_pp =
     match t with
@@ -88,12 +94,17 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
     | Ast.AttributedTerm (_, term) -> pp_term ~pp_parens:false term
     | Ast.Appl terms ->
         sprintf "%s" (String.concat " " (List.map pp_term terms))
-    | Ast.Binder (`Forall, (Ast.Ident ("_", None), typ), body)
-    | Ast.Binder (`Pi, (Ast.Ident ("_", None), typ), body) ->
+    | Ast.Binder (`Forall, (Ast.Ident ("_", `Ambiguous), typ), body)
+    | Ast.Binder (`Forall, (Ast.Ident ("_", `Rel), typ), body)
+    | Ast.Binder (`Pi, (Ast.Ident ("_", `Ambiguous), typ), body) 
+    | Ast.Binder (`Pi, (Ast.Ident ("_", `Rel), typ), body) ->
         sprintf "%s \\to %s"
           (match typ with None -> "?" | Some typ -> pp_term typ)
           (pp_term ~pp_parens:true body)
     | Ast.Binder (kind, var, body) ->
+(*
+ * sprintf "\\%s[%s] %s.%s" (pp_binder kind) (pp_ident var) (pp_capture_variable pp_term var)
+ *)
         sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable pp_term var)
           (pp_term ~pp_parens:true body)
     | Ast.Case (term, indtype, typ, patterns) ->
@@ -138,13 +149,9 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
           (match kind with `Inductive -> "rec" | `CoInductive -> "corec")
           (String.concat " and " (List.map map definitions))
           (pp_term term)
-    | Ast.Ident (name, Some []) | Ast.Ident (name, None)
-    | Ast.Uri (name, Some []) | Ast.Uri (name, None) -> name
+    | Ast.Ident (name, _ ) -> pp_ident t
     | Ast.NRef nref -> NReference.string_of_reference nref
     | Ast.NCic cic -> status#ppterm ~metasenv:[] ~context:[] ~subst:[] cic
-    | Ast.Ident (name, Some substs)
-    | Ast.Uri (name, Some substs) ->
-        sprintf "%s \\subst [%s]" name (pp_substs status substs)
     | Ast.Implicit `Vector -> "…"
     | Ast.Implicit `JustOne -> "?"
     | Ast.Implicit (`Tagged name) -> "?"^name
@@ -171,9 +178,8 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
     | true, Ast.Implicit _
     | true, Ast.UserInput
     | true, Ast.Sort _
-    | true, Ast.Ident (_, Some []) 
-    | true, Ast.Ident (_, None)    -> t_pp
-    | _                            -> sprintf "(%s)" t_pp
+    | true, Ast.Ident _    -> t_pp
+    | _                    -> sprintf "(%s)" t_pp
 
 and pp_subst status (name, term) =
  sprintf "%s \\Assign %s" name (pp_term status term)