Added NotationPt.name_of_obj.

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

diff --git a/matitaB/components/content/notationPt.ml b/matitaB/components/content/notationPt.ml
index cead5e7ae8eda28cc6ec9d5fc8262b522ae6f3b6..7cdb86c80b2afe99c2678af993a7038c5a0d6f84 100644 (file)
--- a/matitaB/components/content/notationPt.ml
+++ b/matitaB/components/content/notationPt.ml
@@ -51,9 +51,9 @@ type term_attribute =
   ]
 
 type literal =
-  [ `Symbol of string
-  | `Keyword of string
-  | `Number of string
+  [ `Symbol of string * (string option * string option)
+  | `Keyword of string * (string option * string option)
+  | `Number of string * (string option * string option)
   ]
 
 type case_indtype = string * href option
@@ -62,7 +62,7 @@ type 'term capture_variable = 'term * 'term option
 
 (** To be increased each time the term type below changes, used for "safe"
  * marshalling *)
-let magic = 6
+let magic = 8
 
 type term =
   (* CIC AST *)
@@ -78,26 +78,32 @@ type term =
   | LetIn of term capture_variable * term * term  (* name, body, where *)
   | LetRec of induction_kind * (term capture_variable list * term capture_variable * term * int) list * term
       (* (params, name, body, decreasing arg) list, where *)
-  | Ident of string * subst list option
-      (* literal, substitutions.
-      * Some [] -> user has given an empty explicit substitution list 
-      * None -> user has given no explicit substitution list *)
+  | Ident of string * [ `Ambiguous | `Uri of string | `Rel ]
+      (* literal, disambiguation info (can be ambiguous, a disambiguated uri, 
+       * or an identifier to be converted in a Rel)
+       * case `Uri is also used for literal uris
+       * the parser fills the name of the identifier using the final part of the
+       * uri
+       *)
   | Implicit of [`Vector | `JustOne | `Tagged of string]
   | Meta of int * meta_subst list
-  | Num of string * int (* literal, instance *)
+  | Num of string * (string option * string) option 
+      (* literal, (uri, interpretation name) *)
   | Sort of sort_kind
-  | Symbol of string * int  (* canonical name, instance *)
-
+  (* XXX: symbols used to be packed with their instance number, probably for
+   * disambiguation purposes; hopefully we won't need this info any more *)
+  | Symbol of string * (string option * string) option 
+      (* canonical name, (uri, interpretation name) *)
   | UserInput (* place holder for user input, used by MatitaConsole, not to be
               used elsewhere *)
-  | Uri of string * subst list option (* as Ident, for long names *)
   | NRef of NReference.reference
 
   | NCic of NCic.term
 
   (* Syntax pattern extensions *)
-
-  | Literal of literal
+  (* string option = optional name of an Ast.Symbol occurring in the level 2
+   * term, which is associated to this literal *)
+  | Literal of (string option * literal)
   | Layout of layout_pattern
 
   | Magic of magic_term
@@ -188,6 +194,38 @@ type 'term obj =
   | Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list
       (** left parameters, name, type, fields *)
 
+let name_of_obj = function
+  | Theorem (_,n,_,_,_) | Record (_,n,_,_)
+  | Inductive (_,(n,_,_,_)::_) -> n
+  | _ -> (* empty inductive block *) assert false
+;;
+ 
+let map_variable f (t,u) = f t, HExtlib.map_option f u ;;
+
+let map_pattern f = function
+  | Pattern (s,h,vl) -> Pattern (s,h,List.map (map_variable f) vl)
+  | p -> p
+;;
+
+let map f = function
+  | AttributedTerm (a,u) -> AttributedTerm (a,f u)
+  | Appl tl -> Appl (List.map f tl)
+  | Binder (k,n,body) -> Binder (k,map_variable f n,f body)
+  | Case (t,ity,oty,pl) -> 
+      let pl' = List.map (fun (p,u) -> map_pattern f p, f u) pl in 
+      Case (f t,ity,HExtlib.map_option f oty,pl')
+  | Cast (u,v) -> Cast (f u,f v)
+  | LetIn (n,u,v) -> LetIn (n,f u,f v)
+  | LetRec (ik,l,t) ->
+      let l' = List.map (fun (vl,v,u,n) -> 
+                (List.map (map_variable f) vl,
+                 map_variable f v,
+                 f u,
+                 n)) l
+      in LetRec (ik,l',f t)
+  | t -> t
+;;
+
 (** {2 Standard precedences} *)
 
 let let_in_prec = 10
@@ -195,3 +233,11 @@ let binder_prec = 20
 let apply_prec = 70
 let simple_prec = 90
 
+(* sequents *)
+
+type context_entry = 
+    Decl of term
+  | Def of term * term 
+
+type sequent = int * context * term
+and context = (string * context_entry) list