diff options
Diffstat (limited to 'contrib/xml')
| -rw-r--r-- | contrib/xml/cic2acic.ml | 19 | ||||
| -rw-r--r-- | contrib/xml/doubleTypeInference.ml | 30 | ||||
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 39 |
3 files changed, 54 insertions, 34 deletions
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index ff07c3c4..8a5967a2 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -22,8 +22,13 @@ let get_module_path_of_section_path path = List.filter (function modul -> Libnames.is_dirpath_prefix_of modul dirpath) modules with - [modul] -> modul - | _ -> raise TwoModulesWhoseDirPathIsOneAPrefixOfTheOther + [] -> + Pp.warning ("Modules not supported: reference to "^ + Libnames.string_of_path path^" will be wrong"); + dirpath + | [modul] -> modul + | _ -> + raise TwoModulesWhoseDirPathIsOneAPrefixOfTheOther ;; (*CSC: Problem: here we are using the wrong (???) hypothesis that there do *) @@ -652,11 +657,13 @@ print_endline "PASSATO" ; flush stdout ; A.ALambdas (new_passed_lambdas, t') ) | T.LetIn (n,s,t,d) -> - let n' = + let id = match n with - N.Anonymous -> N.Anonymous - | _ -> - N.Name (Nameops.next_name_away n (Termops.ids_of_context env)) + N.Anonymous -> N.id_of_string "_X" + | N.Name id -> id + in + let n' = + N.Name (Nameops.next_ident_away id (Termops.ids_of_context env)) in Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; let sourcesort = diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml index c7d3b4ff..cce78891 100644 --- a/contrib/xml/doubleTypeInference.ml +++ b/contrib/xml/doubleTypeInference.ml @@ -26,31 +26,13 @@ let cprop = (N.mk_label "CProp") ;; -let whd_betadeltaiotacprop env evar_map ty = +let whd_betadeltaiotacprop env _evar_map ty = let module R = Rawterm in - let red_exp = - R.Hnf (*** Instead CProp is made Opaque ***) -(* - R.Cbv - {R.rBeta = true ; R.rIota = true ; R.rDelta = true; R.rZeta=true ; - R.rConst = [Names.EvalConstRef cprop] - } -*) - in -Conv_oracle.set_opaque_const cprop; -prerr_endline "###whd_betadeltaiotacprop:" ; -let xxx = -(*Pp.msgerr (Printer.pr_lconstr_env env ty);*) -prerr_endline ""; - (fst (Redexpr.reduction_of_red_expr red_exp)) env evar_map ty -in -prerr_endline "###FINE" ; -(* -Pp.msgerr (Printer.pr_lconstr_env env xxx); -*) -prerr_endline ""; -Conv_oracle.set_transparent_const cprop; -xxx + let module C = Closure in + let module CR = C.RedFlags in + (*** CProp is made Opaque ***) + let flags = CR.red_sub C.betadeltaiota (CR.fCONST cprop) in + C.whd_val (C.create_clos_infos flags env) (C.inject ty) ;; diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index f286d2c8..01271323 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -461,11 +461,42 @@ let kind_of_constant kn = match Declare.constant_kind (Nametab.sp_of_global(Libnames.ConstRef kn)) with | DK.IsAssumption DK.Definitional -> "AXIOM","Declaration" | DK.IsAssumption DK.Logical -> "AXIOM","Axiom" - | DK.IsAssumption DK.Conjectural -> "AXIOM","Conjecture" + | DK.IsAssumption DK.Conjectural -> + Pp.warning "Conjecture not supported in dtd (used Declaration instead)"; + "AXIOM","Declaration" | DK.IsDefinition DK.Definition -> "DEFINITION","Definition" - | DK.IsDefinition DK.Example -> "DEFINITION","Example" - | DK.IsDefinition _ -> Util.anomaly "Unsupported constant kind" - | DK.IsProof thm -> "THEOREM",DK.string_of_theorem_kind thm + | DK.IsDefinition DK.Example -> + Pp.warning "Example not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.Coercion -> + Pp.warning "Coercion not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.SubClass -> + Pp.warning "SubClass not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.CanonicalStructure -> + Pp.warning "CanonicalStructure not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.Fixpoint -> + Pp.warning "Fixpoint not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.CoFixpoint -> + Pp.warning "CoFixpoint not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.Scheme -> + Pp.warning "Scheme not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.StructureComponent -> + Pp.warning "StructureComponent not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.IdentityCoercion -> + Pp.warning "IdentityCoercion not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) -> + "THEOREM",DK.string_of_theorem_kind thm + | DK.IsProof _ -> + Pp.warning "Unsupported theorem kind (used Theorem instead)"; + "THEOREM",DK.string_of_theorem_kind DK.Theorem ;; let kind_of_global r = |