X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicParser.ml;h=3962323a18767d0faa087f486b44d768cbfa901e;hb=HEAD;hp=150fe4ad983f6dab3bad1d117877e6093531b755;hpb=abd2098b6c4a40b36bb4b950c607eb4b4a7852bc;p=helm.git diff --git a/helm/software/components/cic/cicParser.ml b/helm/software/components/cic/cicParser.ml index 150fe4ad9..3962323a1 100644 --- 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} *)