s/LocatedTerm/AnnotatedTerm + various annotations/

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 08bbf43ebcc01ea4e06c2e67cd5b6e654018d48c..2806becc152a89d10798d26d7a4a6737efb08359 100644 (file)
--- 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 1b5933f7dd3be255222487e3e8993dde68f027fd..849d102850966e7d80d09ba918108b2b5d1db2ce 100644 (file)
--- 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 896e1dcc32cff08cf973e8671b0e8f53f81f1e3b..411159b2fcd681e3b255b88242acf2f150a5224d 100644 (file)
--- 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 e8d3e58f15e303607496d1f82ada36d754de7fa5..b2b7149758731ea770afa671b135e54204c6a4a4 100644 (file)
--- 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) =