From: Stefano Zacchiroli 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) =