parameter sintax added to axiom statement

[helm.git] / helm / software / components / cic / cicParser.ml

diff --git a/helm/software/components/cic/cicParser.ml b/helm/software/components/cic/cicParser.ml
index 150fe4ad983f6dab3bad1d117877e6093531b755..3962323a18767d0faa087f486b44d768cbfa901e 100644 (file)
--- a/helm/software/components/cic/cicParser.ml
+++ b/helm/software/components/cic/cicParser.ml
@@ -60,7 +60,7 @@ type stack_entry =
       (* id, name, type, body *)
   | Constructor of string * Cic.annterm   (* name, type *)
   | Decl of Cic.id * Cic.name * Cic.annterm (* id, binder, source *)
-  | Def of Cic.id * Cic.name * Cic.annterm  (* id, binder, source *)
+  | Def of Cic.id * Cic.name * Cic.annterm * Cic.annterm  (* id, binder, source, type *)
   | Fix_fun of Cic.id * string * int * Cic.annterm * Cic.annterm
       (* id, name, ind. index, type, body *)
   | Inductive_type of string * string * bool * Cic.annterm *
@@ -97,7 +97,7 @@ let string_of_stack ctxt =
       | Constructor (name, _) -> "Constructor " ^ name
       | Cofix_fun (id, _, _, _) -> sprintf "Cofix_fun (id=%s)" id
       | Decl (id, _, _) -> sprintf "Decl (id=%s)" id
-      | Def (id, _, _) -> sprintf "Def (id=%s)" id
+      | Def (id, _, _, _) -> sprintf "Def (id=%s)" id
       | Fix_fun (id, _, _, _, _) -> sprintf "Fix_fun (id=%s)" id
       | Inductive_type (id, name, _, _, _) ->
           sprintf "Inductive_type %s (id=%s)" name id
@@ -296,23 +296,30 @@ let uri_list_of_string =
   fun s ->
     List.map uri_of_string (Str.split space_RE s)
 
+let impredicative_set = ref true;;
+
 let sort_of_string ctxt = function
   | "Prop" -> Cic.Prop
-  | "Set"  -> Cic.Set
-  | "CProp" -> Cic.CProp
   (* THIS CASE IS HERE ONLY TO ALLOW THE PARSING OF COQ LIBRARY
    * THIS SHOULD BE REMOVED AS SOON AS univ_maker OR COQ'S EXPORTATION 
    * IS FIXED *)
+  | "CProp" -> Cic.CProp (CicUniv.fresh ~uri:ctxt.uri ())
   | "Type" ->  Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
+  | "Set" when !impredicative_set -> Cic.Set
+  | "Set" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
   | s ->
       let len = String.length s in
-      if not(len > 5) then parse_error ctxt "sort expected";
-      if not(String.sub s 0 5 = "Type:") then parse_error ctxt "sort expected";
-      try 
-        Cic.Type 
-          (CicUniv.fresh 
-            ~uri:ctxt.uri 
-            ~id:(int_of_string (String.sub s 5 (len - 5))) ())
+      let sort_len, mk_sort = 
+        if len > 5 && String.sub s 0 5 = "Type:" then 5,fun x -> Cic.Type x 
+        else if len > 6 && String.sub s 0 6 = "CProp:" then 6,fun x->Cic.CProp x
+        else parse_error ctxt "sort expected"
+      in
+      let s = String.sub s sort_len (len - sort_len) in
+      let i = String.index s ':' in  
+      let id =  int_of_string (String.sub s 0 i) in
+      let suri = String.sub s (i+1) (len - sort_len - i - 1) in
+      let uri = UriManager.uri_of_string suri in
+      try mk_sort (CicUniv.fresh ~uri ~id ())
       with
       | Failure "int_of_string" 
       | Invalid_argument _ -> parse_error ctxt "sort expected" 
@@ -406,14 +413,22 @@ let end_element ctxt tag =
         | ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source)
         | _ -> attribute_error ())
   | "def" ->  (* same as "decl" above *)
-      let source = pop_cic ctxt in
+      let ty,source =
+       (*CSC: hack to parse Coq files where the LetIn is not typed *)
+       let ty = pop_cic ctxt in
+       try
+        let source = pop_cic ctxt in
+         ty,source
+       with
+        Parser_failure _ -> Cic.AImplicit ("MISSING_def_TYPE",None),ty
+      in
       push ctxt
         (match pop_tag_attrs ctxt with
         | ["binder", binder; "id", id]
         | ["binder", binder; "id", id; "sort", _] ->
-            Def (id, Cic.Name binder, source)
+            Def (id, Cic.Name binder, source, ty)
         | ["id", id]
-        | ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source)
+        | ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source, ty)
         | _ -> attribute_error ())
   | "arity"           (* transparent elements (i.e. which contain a CIC) *)
   | "body"
@@ -467,8 +482,8 @@ let end_element ctxt tag =
   | "LETIN" ->
       let target = pop_cic ctxt in
       let rec add_def target = function
-        | Def (id, binder, source) :: tl ->
-            add_def (Cic.ALetIn (id, binder, source, target)) tl
+        | Def (id, binder, source, ty) :: tl ->
+            add_def (Cic.ALetIn (id, binder, source, ty, target)) tl
         | tl ->
             ctxt.stack <- tl;
             target
@@ -667,6 +682,7 @@ let end_element ctxt tag =
       push ctxt 
         (match pop_tag_attrs ctxt with
         | [ "value", "definition"] -> Obj_flavour `Definition
+        | [ "value", "mutual_definition"] -> Obj_flavour `MutualDefinition
         | [ "value", "fact"] -> Obj_flavour `Fact
         | [ "value", "lemma"] -> Obj_flavour `Lemma
         | [ "value", "remark"] -> Obj_flavour `Remark
@@ -678,13 +694,6 @@ let end_element ctxt tag =
       let class_modifiers = pop_class_modifiers ctxt in
       push ctxt
         (match pop_tag_attrs ctxt with
-        | ["value", "coercion"] -> Obj_class (`Coercion 0)
-        | ("value", "coercion")::["arity",n]  
-        | ("arity",n)::["value", "coercion"] -> 
-            let arity = try int_of_string n with Failure _ ->
-              parse_error "\"arity\" must be an integer"
-            in
-            Obj_class (`Coercion arity)
         | ["value", "elim"] ->
             (match class_modifiers with
             | [Cic_term (Cic.ASort (_, sort))] -> Obj_class (`Elim sort)
@@ -716,7 +725,8 @@ let end_element ctxt tag =
             in
             Obj_class (`Record fields)
         | ["value", "projection"] -> Obj_class `Projection
-        | _ -> attribute_error ())
+        | ["value", "inversion"] -> Obj_class `InversionPrinciple
+       | _ -> attribute_error ())
   | tag ->
       match find_helm_exception ctxt with
       | Some (exn, arg) -> raise (Getter_failure (exn, arg))
@@ -770,7 +780,7 @@ let parse uri filename =
   | Getter_failure _ as exn ->
       raise exn
   | exn ->
-      raise (Parser_failure ("uncaught exception: " ^ Printexc.to_string exn))
+      raise (Parser_failure ("CicParser: uncaught exception: " ^ Printexc.to_string exn))
 
 (** {2 API implementation} *)