From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 3 Feb 2004 14:06:01 +0000 (+0000)
Subject: s/LocatedTerm/AnnotatedTerm + various annotations/
X-Git-Tag: V_0_2_3~96
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4b44277b39e8a30741e544d9c3cee349d7c61ce0;p=helm.git

s/LocatedTerm/AnnotatedTerm + various annotations/
---

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 08bbf43eb..2806becc1 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -46,7 +46,8 @@ let term0 = Grammar.Entry.create grammar "term0"
 (* let tactic = Grammar.Entry.create grammar "tactic" *)
 (* let tactical = Grammar.Entry.create grammar "tactical" *)
 
-let return_term loc term = CicTextualParser2Ast.LocatedTerm (loc, term)
+let return_term loc term =
+  CicTextualParser2Ast.AttributedTerm (`Loc loc, term)
 (* let return_term loc term = term *)
 
 let fail (x, y) msg =
diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2Ast.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2Ast.mli
index 1b5933f7d..849d10285 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2Ast.mli
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2Ast.mli
@@ -63,8 +63,13 @@ type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ]
 type induction_kind = [ `Inductive | `CoInductive ]
 type sort_kind = [ `Prop | `Set | `Type | `CProp ]
 
+type term_attribute =
+  [ `Loc of location  (* source file location *)
+  | `IdRef of string  (* ACic pointer *)
+  ]
+
 type term =
-  | LocatedTerm of location * term
+  | AttributedTerm of term_attribute * term
 
   | Appl of term list
   | Appl_symbol of string * int * term list (* literal, instance, args *)
diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.ml
index 896e1dcc3..411159b2f 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.ml
@@ -37,9 +37,7 @@ let rec pp_capture_variable = function
   | name, None -> pp_name name
   | name, Some typ -> "(" ^ pp_name name ^ ": " ^ pp_term typ ^ ")"
 and pp_term = function
-  | LocatedTerm ((p_begin, p_end), term) ->
-(*       sprintf "[%d,%d]%s" p_begin p_end (pp_term term) *)
-      pp_term term
+  | AttributedTerm (_, term) -> pp_term term
 
   | Appl terms -> sprintf "(%s)" (String.concat " " (List.map pp_term terms))
   | Appl_symbol (symbol, _, terms) ->
diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index e8d3e58f1..b2b714975 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -75,7 +75,9 @@ let find_in_environment name context =
 
 let interpretate ~context ~env ast =
   let rec aux loc context = function
-    | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
+    | CicTextualParser2Ast.AttributedTerm (`Loc loc, term) ->
+        aux loc context term
+    | CicTextualParser2Ast.AttributedTerm (_, term) -> aux loc context term
     | CicTextualParser2Ast.Appl terms ->
         Cic.Appl (List.map (aux loc context) terms)
     | CicTextualParser2Ast.Appl_symbol (symb, i, args) ->
@@ -190,12 +192,14 @@ let interpretate ~context ~env ast =
     | Some term -> aux loc context term
   in
   match ast with
-  | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
+  | CicTextualParser2Ast.AttributedTerm (`Loc loc, term) -> aux loc context term
   | _ -> assert false
 
 let domain_of_term ~context ast =
   let rec aux loc context = function
-    | CicTextualParser2Ast.LocatedTerm (_, term) -> aux loc context term
+    | CicTextualParser2Ast.AttributedTerm (`Loc loc, term) ->
+        aux loc context term
+    | CicTextualParser2Ast.AttributedTerm (_, term) -> aux loc context term
     | CicTextualParser2Ast.Appl terms ->
         List.fold_left (fun dom term -> Domain.union dom (aux loc context term))
           Domain.empty terms
@@ -269,7 +273,7 @@ let domain_of_term ~context ast =
     | Some t -> aux loc context t
   in
   match ast with
-  | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
+  | CicTextualParser2Ast.AttributedTerm (`Loc loc, term) -> aux loc context term
   | _ -> assert false
 
 module Make (C: Callbacks) =