X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FcicAst.ml;h=ca48567863aa8d9c88ebf6eba9aa986db55c1fae;hb=fdd8107cc53f5e862004aa5fcd48593ee5634234;hp=fcc80369794c375c8bbe0b8d825d8cece1f2b701;hpb=e3ce9e2940a9e9c736209517e20e4c4292fdd0c3;p=helm.git

diff --git a/helm/ocaml/cic_transformations/cicAst.ml b/helm/ocaml/cic_transformations/cicAst.ml
index fcc803697..ca4856786 100644
--- a/helm/ocaml/cic_transformations/cicAst.ml
+++ b/helm/ocaml/cic_transformations/cicAst.ml
@@ -23,12 +23,19 @@
  * http://helm.cs.unibo.it/
  *)
 
-(** {2 Parsing related types} *)
+open Printf
 
 type location = Lexing.position * Lexing.position
 
-  (* maps old style (i.e. <= 3.07) lexer location to new style location, padding
-  * with dummy values where needed *)
+let pp_location (loc_begin, loc_end) =
+  let c_begin = loc_begin.Lexing.pos_cnum - loc_begin.Lexing.pos_bol in
+  let c_end = loc_end.Lexing.pos_cnum - loc_end.Lexing.pos_bol in
+  if loc_begin.Lexing.pos_lnum = -1 || loc_end.Lexing.pos_lnum = -1 then
+      sprintf "%d-%d" c_begin c_end
+    else
+      sprintf "(%d,%d)-(%d,%d)" loc_begin.Lexing.pos_lnum c_begin
+        loc_end.Lexing.pos_lnum c_end
+
 let floc_of_loc (loc_begin, loc_end) =
   let floc_begin =
     { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
@@ -37,46 +44,51 @@ let floc_of_loc (loc_begin, loc_end) =
   let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in
   (floc_begin, floc_end)
 
-  (* the other way round *)
 let loc_of_floc = function
   | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } ->
       (loc_begin, loc_end)
 
 let dummy_floc = floc_of_loc (-1, -1)
 
-(** {2 Cic Ast} *)
-
 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 *)
+  [ `Loc of location
+  | `IdRef of string
   ]
 
 type term =
   | AttributedTerm of term_attribute * term
 
   | Appl of term list
-  | Binder of binder_kind * capture_variable * term (* kind, name, body *)
+  | Binder of binder_kind * capture_variable * term
   | Case of term * string option * term option * (case_pattern * term) list
-      (* what to match, inductive type, out type, <pattern,action> list *)
-  | LetIn of capture_variable * term * term  (* name, body, where *)
+  | LetIn of capture_variable * term * term
   | LetRec of induction_kind * (capture_variable * term * int) list * term
-      (* (name, body, decreasing argument) 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 *)
   | Implicit
   | Meta of int * meta_subst list
-  | Num of string * int (* literal, instance *)
+  | Num of string * int
   | Sort of sort_kind
-  | Symbol of string * int  (* canonical name, instance *)
+  | Symbol of string * int
+
+  | UserInput
+  | Uri of string * subst list option
 
-and capture_variable = Cic.name * term option (* name, type *)
+and capture_variable = Cic.name * term option
 and meta_subst = term option
 and subst = string * term
 and case_pattern = string * capture_variable list
 
+let pack asts =
+  List.fold_right
+    (fun ast acc -> Binder (`Forall, (Cic.Anonymous, Some ast), acc))
+    asts (Sort `Type)
+
+let rec unpack = function
+  | Binder (`Forall, (Cic.Anonymous, Some ast), Sort `Type) -> [ast]
+  | Binder (`Forall, (Cic.Anonymous, Some ast), tgt) -> ast :: unpack tgt
+  | _ -> assert false
+