From 86b0a224bd9251ed22648de04bc0d00f11dbd0fc Mon Sep 17 00:00:00 2001 From: matitaweb Date: Mon, 12 Mar 2012 14:56:10 +0000 Subject: [PATCH] --- matitaB/components/content/.depend | 22 ++--- matitaB/components/content_pres/.depend | 48 +++++----- .../content_pres/cicNotationParser.ml | 6 +- matitaB/components/disambiguation/.depend | 17 ++-- .../components/disambiguation/disambiguate.ml | 51 ++++++----- .../disambiguation/disambiguate.mli | 5 +- matitaB/components/extlib/.depend | 54 ++++++------ matitaB/components/getter/.depend | 52 +++++------ matitaB/components/grafite/.depend | 10 +-- matitaB/components/grafite_engine/.depend | 18 ++-- .../grafite_engine/grafiteEngine.ml | 64 +++++++++++++- matitaB/components/grafite_parser/.depend | 12 +-- .../grafite_parser/print_grammar.ml | 6 +- matitaB/components/library/.depend | 18 ++-- matitaB/components/logger/.depend | 6 +- matitaB/components/ng_cic_content/.depend | 12 +-- matitaB/components/ng_disambiguation/.depend | 24 ++--- .../ng_disambiguation/grafiteDisambiguate.ml | 4 +- .../ng_disambiguation/nCicDisambiguate.ml | 4 +- matitaB/components/ng_kernel/.depend | 58 ++++++------- matitaB/components/ng_library/.depend | 6 +- matitaB/components/ng_library/nCicLibrary.ml | 87 +++++++++++++------ matitaB/components/ng_library/nCicLibrary.mli | 3 +- matitaB/components/ng_paramodulation/.depend | 78 ++++++++--------- matitaB/components/ng_refiner/.depend | 42 ++++----- matitaB/components/ng_refiner/nCicRefiner.ml | 9 +- .../components/ng_refiner/nCicUnification.ml | 2 +- matitaB/components/ng_tactics/.depend | 48 +++++----- matitaB/components/ng_tactics/nDestructTac.ml | 9 +- matitaB/components/registry/.depend | 6 +- matitaB/components/syntax_extensions/.depend | 10 +-- .../syntax_extensions/make_table.ml | 2 +- matitaB/components/thread/.depend | 12 +-- matitaB/components/xml/.depend | 12 +-- matitaB/matita/html/register.html | 27 ++++++ matitaB/matita/matitaEngine.ml | 8 +- 36 files changed, 494 insertions(+), 358 deletions(-) create mode 100755 matitaB/matita/html/register.html diff --git a/matitaB/components/content/.depend b/matitaB/components/content/.depend index 6d0eb1f22..70c507598 100644 --- a/matitaB/components/content/.depend +++ b/matitaB/components/content/.depend @@ -1,13 +1,13 @@ -notationUtil.cmi: notationPt.cmo -notationEnv.cmi: notationPt.cmo -notationPp.cmi: notationPt.cmo notationEnv.cmi -notationPt.cmo: -notationPt.cmx: -notationUtil.cmo: notationPt.cmo notationUtil.cmi -notationUtil.cmx: notationPt.cmx notationUtil.cmi -notationEnv.cmo: notationUtil.cmi notationPt.cmo notationEnv.cmi -notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi +notationUtil.cmi: notationPt.cmo +notationEnv.cmi: notationPt.cmo +notationPp.cmi: notationPt.cmo notationEnv.cmi +notationPt.cmo: +notationPt.cmx: +notationUtil.cmo: notationPt.cmo notationUtil.cmi +notationUtil.cmx: notationPt.cmx notationUtil.cmi +notationEnv.cmo: notationUtil.cmi notationPt.cmo notationEnv.cmi +notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi notationPp.cmo: notationUtil.cmi notationPt.cmo notationEnv.cmi \ - notationPp.cmi + notationPp.cmi notationPp.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmx \ - notationPp.cmi + notationPp.cmi diff --git a/matitaB/components/content_pres/.depend b/matitaB/components/content_pres/.depend index 3a1c6036d..2d171b1f5 100644 --- a/matitaB/components/content_pres/.depend +++ b/matitaB/components/content_pres/.depend @@ -1,26 +1,26 @@ -cicNotationLexer.cmi: -smallLexer.cmi: -cicNotationParser.cmi: -box.cmi: -content2presMatcher.cmi: -termContentPres.cmi: cicNotationParser.cmi -boxPp.cmi: cicNotationPres.cmi -cicNotationPres.cmi: termContentPres.cmi box.cmi -cicNotationLexer.cmo: cicNotationLexer.cmi -cicNotationLexer.cmx: cicNotationLexer.cmi -smallLexer.cmo: smallLexer.cmi -smallLexer.cmx: smallLexer.cmi -cicNotationParser.cmo: cicNotationLexer.cmi cicNotationParser.cmi -cicNotationParser.cmx: cicNotationLexer.cmx cicNotationParser.cmi -box.cmo: box.cmi -box.cmx: box.cmi -content2presMatcher.cmo: content2presMatcher.cmi -content2presMatcher.cmx: content2presMatcher.cmi +cicNotationLexer.cmi: +smallLexer.cmi: +cicNotationParser.cmi: +box.cmi: +content2presMatcher.cmi: +termContentPres.cmi: cicNotationParser.cmi +boxPp.cmi: cicNotationPres.cmi +cicNotationPres.cmi: termContentPres.cmi box.cmi +cicNotationLexer.cmo: cicNotationLexer.cmi +cicNotationLexer.cmx: cicNotationLexer.cmi +smallLexer.cmo: smallLexer.cmi +smallLexer.cmx: smallLexer.cmi +cicNotationParser.cmo: cicNotationLexer.cmi cicNotationParser.cmi +cicNotationParser.cmx: cicNotationLexer.cmx cicNotationParser.cmi +box.cmo: box.cmi +box.cmx: box.cmi +content2presMatcher.cmo: content2presMatcher.cmi +content2presMatcher.cmx: content2presMatcher.cmi termContentPres.cmo: content2presMatcher.cmi cicNotationParser.cmi \ - termContentPres.cmi + termContentPres.cmi termContentPres.cmx: content2presMatcher.cmx cicNotationParser.cmx \ - termContentPres.cmi -boxPp.cmo: box.cmi boxPp.cmi -boxPp.cmx: box.cmx boxPp.cmi -cicNotationPres.cmo: termContentPres.cmi box.cmi cicNotationPres.cmi -cicNotationPres.cmx: termContentPres.cmx box.cmx cicNotationPres.cmi + termContentPres.cmi +boxPp.cmo: box.cmi boxPp.cmi +boxPp.cmx: box.cmx boxPp.cmi +cicNotationPres.cmo: termContentPres.cmi box.cmi cicNotationPres.cmi +cicNotationPres.cmx: termContentPres.cmx box.cmx cicNotationPres.cmi diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml index 7522d3c79..6736211d4 100644 --- a/matitaB/components/content_pres/cicNotationParser.ml +++ b/matitaB/components/content_pres/cicNotationParser.ml @@ -30,6 +30,8 @@ open Printf module Ast = NotationPt module Env = NotationEnv +let prerr_endline _ = () + exception Parse_error of string exception Level_not_found of int @@ -322,9 +324,9 @@ let extract_term_production status pattern = | Ast.List0 (_, None) -> Gramext.Slist0 s | Ast.List1 (_, None) -> Gramext.Slist1 s | Ast.List0 (_, Some l) -> - Gramext.Slist0sep (s, gram_of_literal status l) + Gramext.Slist0sep (s, gram_of_literal status l,true) | Ast.List1 (_, Some l) -> - Gramext.Slist1sep (s, gram_of_literal status l) + Gramext.Slist1sep (s, gram_of_literal status l,true) | _ -> assert false in [ Env (List.map Env.list_declaration p_names), diff --git a/matitaB/components/disambiguation/.depend b/matitaB/components/disambiguation/.depend index 9fdbeeeaf..6025cd249 100644 --- a/matitaB/components/disambiguation/.depend +++ b/matitaB/components/disambiguation/.depend @@ -1,11 +1,6 @@ -disambiguateTypes.cmi: -disambiguate.cmi: disambiguateTypes.cmi -multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi -disambiguateTypes.cmo: disambiguateTypes.cmi -disambiguateTypes.cmx: disambiguateTypes.cmi -disambiguate.cmo: disambiguateTypes.cmi disambiguate.cmi -disambiguate.cmx: disambiguateTypes.cmx disambiguate.cmi -multiPassDisambiguator.cmo: disambiguateTypes.cmi disambiguate.cmi \ - multiPassDisambiguator.cmi -multiPassDisambiguator.cmx: disambiguateTypes.cmx disambiguate.cmx \ - multiPassDisambiguator.cmi +disambiguateTypes.cmi: +disambiguate.cmi: disambiguateTypes.cmi +disambiguateTypes.cmo: disambiguateTypes.cmi +disambiguateTypes.cmx: disambiguateTypes.cmi +disambiguate.cmo: disambiguateTypes.cmi disambiguate.cmi +disambiguate.cmx: disambiguateTypes.cmx disambiguate.cmi diff --git a/matitaB/components/disambiguation/disambiguate.ml b/matitaB/components/disambiguation/disambiguate.ml index e78ca54a3..7e395e1c1 100644 --- a/matitaB/components/disambiguation/disambiguate.ml +++ b/matitaB/components/disambiguation/disambiguate.ml @@ -31,10 +31,7 @@ open DisambiguateTypes module Ast = NotationPt -(* hard errors, spurious errors *) -exception NoWellTypedInterpretation of - ((Stdpp.location * string) list * - (Stdpp.location * string) list) +exception NoWellTypedInterpretation of (Stdpp.location * string) exception PathNotWellFormed @@ -140,8 +137,6 @@ type ('alias,'ast_thing,'metasenv,'subst,'thing,'ugraph) disamb_result = * node; each ast is associated with the actual instantiation of the node, * the refinement error, and the location at which refinement fails *) | Disamb_failure of - (* hard errors, spurious errors *) - (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list * (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list let resolve ~env ~universe ~mk_choice item interpr arg = @@ -623,8 +618,10 @@ let test_interpr ~context ~metasenv ~subst ~use_coercions ~expty ~env ~universe (*| Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg)) | Invalid_choice loc_msg -> Ko loc_msg*) | Invalid_choice x -> - let loc,err = Lazy.force x in Some (loc,err) - | _ -> None + let loc,err = Lazy.force x in + debug_print (lazy ("test_interpr invalid choice: " ^ err)); + Some (loc,err) + | e -> debug_print (lazy ("uncaught error: "^ Printexc.to_string e));None ;; exception Not_ambiguous;; @@ -699,6 +696,8 @@ let rec disambiguate_list "\nin " ^ pp_thing (ctx t))); (* get possible instantiations of t *) let instances = get_instances ctx t in + if instances = [] then + raise (NoWellTypedInterpretation (loc_t, "No choices for " ^ astpp t)); debug_print (lazy "-- possible instances:"); (* List.iter (fun u0 -> debug_print (lazy ("-- instance: " ^ (pp_thing u0)))) @@ -758,27 +757,37 @@ let disambiguate_thing match refine_thing metasenv subst context uri ~use_coercions t' expty base_univ ~localization_tbl with | Ok (t',m',s',u') -> t,m',s',t',u' - | Uncertain x -> - let _,err = Lazy.force x in + | Uncertain x | Ko x -> + let loc,err = Lazy.force x in debug_print (lazy ("refinement uncertain after disambiguation: " ^ err)); - assert false - | _ -> assert false + raise (NoWellTypedInterpretation (loc,err)) in match (test_interpr thing) with | Some (loc,err) -> -(* debug_print (lazy ("preliminary test fail: " ^ pp_thing thing)); *) - Disamb_failure ([[thing,None,loc,err],loc],[]) + debug_print (lazy ("preliminary test fail: " ^ pp_thing thing)); + Disamb_failure ([[thing,None,loc,err],loc]) | None -> let res,errors = aux [thing] in - let res = - HExtlib.filter_map (fun t -> - try Some (refine t) - with _ -> -(* debug_print (lazy ("can't interpretate/refine " ^ (pp_thing t)));*) - None) res + let res,inner_errors = + List.split + (List.map (fun t -> + try (Some (refine t), None) + (* this error is actually a singleton *) + with NoWellTypedInterpretation loc_err -> + debug_print (lazy ("can't interpretate/refine " ^ (pp_thing t))); + None, Some loc_err) res) in + let res = HExtlib.filter_map (fun x -> x) res in + let inner_errors = + HExtlib.filter_map + (function Some (loc,err) -> Some (thing,None,loc,err) | None -> None) + inner_errors + in + let errors = + if inner_errors <> [] then (inner_errors,Stdpp.dummy_loc)::errors + else errors in (match res with - | [] -> Disamb_failure (errors,[]) + | [] -> prerr_endline ((string_of_int (List.length errors)) ^ " error frames");Disamb_failure errors | _ -> Disamb_success res) ;; diff --git a/matitaB/components/disambiguation/disambiguate.mli b/matitaB/components/disambiguation/disambiguate.mli index ab347e164..5df0bffcc 100644 --- a/matitaB/components/disambiguation/disambiguate.mli +++ b/matitaB/components/disambiguation/disambiguate.mli @@ -28,12 +28,9 @@ type ('alias,'ast_thing,'metasenv,'subst,'thing,'ugraph) disamb_result = | Disamb_success of ('ast_thing * 'metasenv * 'subst * 'thing * 'ugraph) list | Disamb_failure of - (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list * (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list -exception NoWellTypedInterpretation of - ((Stdpp.location * string) list * - (Stdpp.location * string) list) +exception NoWellTypedInterpretation of (Stdpp.location * string) exception PathNotWellFormed diff --git a/matitaB/components/extlib/.depend b/matitaB/components/extlib/.depend index 6f707effc..b121fbcd1 100644 --- a/matitaB/components/extlib/.depend +++ b/matitaB/components/extlib/.depend @@ -1,27 +1,27 @@ -componentsConf.cmi: -hExtlib.cmi: -hMarshal.cmi: -patternMatcher.cmi: -hLog.cmi: -trie.cmi: -discrimination_tree.cmi: -hTopoSort.cmi: -graphvizPp.cmi: -componentsConf.cmo: componentsConf.cmi -componentsConf.cmx: componentsConf.cmi -hExtlib.cmo: hExtlib.cmi -hExtlib.cmx: hExtlib.cmi -hMarshal.cmo: hExtlib.cmi hMarshal.cmi -hMarshal.cmx: hExtlib.cmx hMarshal.cmi -patternMatcher.cmo: patternMatcher.cmi -patternMatcher.cmx: patternMatcher.cmi -hLog.cmo: hLog.cmi -hLog.cmx: hLog.cmi -trie.cmo: trie.cmi -trie.cmx: trie.cmi -discrimination_tree.cmo: trie.cmi hExtlib.cmi discrimination_tree.cmi -discrimination_tree.cmx: trie.cmx hExtlib.cmx discrimination_tree.cmi -hTopoSort.cmo: hTopoSort.cmi -hTopoSort.cmx: hTopoSort.cmi -graphvizPp.cmo: graphvizPp.cmi -graphvizPp.cmx: graphvizPp.cmi +componentsConf.cmi: +hExtlib.cmi: +hMarshal.cmi: +patternMatcher.cmi: +hLog.cmi: +trie.cmi: +discrimination_tree.cmi: +hTopoSort.cmi: +graphvizPp.cmi: +componentsConf.cmo: componentsConf.cmi +componentsConf.cmx: componentsConf.cmi +hExtlib.cmo: hExtlib.cmi +hExtlib.cmx: hExtlib.cmi +hMarshal.cmo: hExtlib.cmi hMarshal.cmi +hMarshal.cmx: hExtlib.cmx hMarshal.cmi +patternMatcher.cmo: patternMatcher.cmi +patternMatcher.cmx: patternMatcher.cmi +hLog.cmo: hLog.cmi +hLog.cmx: hLog.cmi +trie.cmo: trie.cmi +trie.cmx: trie.cmi +discrimination_tree.cmo: trie.cmi hExtlib.cmi discrimination_tree.cmi +discrimination_tree.cmx: trie.cmx hExtlib.cmx discrimination_tree.cmi +hTopoSort.cmo: hTopoSort.cmi +hTopoSort.cmx: hTopoSort.cmi +graphvizPp.cmo: graphvizPp.cmi +graphvizPp.cmx: graphvizPp.cmi diff --git a/matitaB/components/getter/.depend b/matitaB/components/getter/.depend index ca64d8ec0..600dc01db 100644 --- a/matitaB/components/getter/.depend +++ b/matitaB/components/getter/.depend @@ -1,38 +1,38 @@ -http_getter_wget.cmi: -http_getter_logger.cmi: -http_getter_misc.cmi: -http_getter_const.cmi: -http_getter_env.cmi: http_getter_types.cmo -http_getter_storage.cmi: -http_getter_common.cmi: http_getter_types.cmo -http_getter.cmi: http_getter_types.cmo -http_getter_types.cmo: -http_getter_types.cmx: -http_getter_wget.cmo: http_getter_types.cmo http_getter_wget.cmi -http_getter_wget.cmx: http_getter_types.cmx http_getter_wget.cmi -http_getter_logger.cmo: http_getter_logger.cmi -http_getter_logger.cmx: http_getter_logger.cmi -http_getter_misc.cmo: http_getter_logger.cmi http_getter_misc.cmi -http_getter_misc.cmx: http_getter_logger.cmx http_getter_misc.cmi -http_getter_const.cmo: http_getter_const.cmi -http_getter_const.cmx: http_getter_const.cmi +http_getter_wget.cmi: +http_getter_logger.cmi: +http_getter_misc.cmi: +http_getter_const.cmi: +http_getter_env.cmi: http_getter_types.cmo +http_getter_storage.cmi: +http_getter_common.cmi: http_getter_types.cmo +http_getter.cmi: http_getter_types.cmo +http_getter_types.cmo: +http_getter_types.cmx: +http_getter_wget.cmo: http_getter_types.cmo http_getter_wget.cmi +http_getter_wget.cmx: http_getter_types.cmx http_getter_wget.cmi +http_getter_logger.cmo: http_getter_logger.cmi +http_getter_logger.cmx: http_getter_logger.cmi +http_getter_misc.cmo: http_getter_logger.cmi http_getter_misc.cmi +http_getter_misc.cmx: http_getter_logger.cmx http_getter_misc.cmi +http_getter_const.cmo: http_getter_const.cmi +http_getter_const.cmx: http_getter_const.cmi http_getter_env.cmo: http_getter_types.cmo http_getter_misc.cmi \ - http_getter_logger.cmi http_getter_const.cmi http_getter_env.cmi + http_getter_logger.cmi http_getter_const.cmi http_getter_env.cmi http_getter_env.cmx: http_getter_types.cmx http_getter_misc.cmx \ - http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi + http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi http_getter_storage.cmo: http_getter_wget.cmi http_getter_types.cmo \ - http_getter_misc.cmi http_getter_env.cmi http_getter_storage.cmi + http_getter_misc.cmi http_getter_env.cmi http_getter_storage.cmi http_getter_storage.cmx: http_getter_wget.cmx http_getter_types.cmx \ - http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi + http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi http_getter_common.cmo: http_getter_types.cmo http_getter_misc.cmi \ - http_getter_logger.cmi http_getter_env.cmi http_getter_common.cmi + http_getter_logger.cmi http_getter_env.cmi http_getter_common.cmi http_getter_common.cmx: http_getter_types.cmx http_getter_misc.cmx \ - http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi + http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi http_getter.cmo: http_getter_wget.cmi http_getter_types.cmo \ http_getter_storage.cmi http_getter_misc.cmi http_getter_logger.cmi \ http_getter_env.cmi http_getter_const.cmi http_getter_common.cmi \ - http_getter.cmi + http_getter.cmi http_getter.cmx: http_getter_wget.cmx http_getter_types.cmx \ http_getter_storage.cmx http_getter_misc.cmx http_getter_logger.cmx \ http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \ - http_getter.cmi + http_getter.cmi diff --git a/matitaB/components/grafite/.depend b/matitaB/components/grafite/.depend index 0e7eba453..ba4fab03a 100644 --- a/matitaB/components/grafite/.depend +++ b/matitaB/components/grafite/.depend @@ -1,5 +1,5 @@ -grafiteAstPp.cmi: grafiteAst.cmo -grafiteAst.cmo: -grafiteAst.cmx: -grafiteAstPp.cmo: grafiteAst.cmo grafiteAstPp.cmi -grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi +grafiteAstPp.cmi: grafiteAst.cmo +grafiteAst.cmo: +grafiteAst.cmx: +grafiteAstPp.cmo: grafiteAst.cmo grafiteAstPp.cmi +grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi diff --git a/matitaB/components/grafite_engine/.depend b/matitaB/components/grafite_engine/.depend index d04ec9d2c..27787b008 100644 --- a/matitaB/components/grafite_engine/.depend +++ b/matitaB/components/grafite_engine/.depend @@ -1,11 +1,11 @@ -grafiteTypes.cmi: -nCicCoercDeclaration.cmi: grafiteTypes.cmi -grafiteEngine.cmi: grafiteTypes.cmi -grafiteTypes.cmo: grafiteTypes.cmi -grafiteTypes.cmx: grafiteTypes.cmi -nCicCoercDeclaration.cmo: grafiteTypes.cmi nCicCoercDeclaration.cmi -nCicCoercDeclaration.cmx: grafiteTypes.cmx nCicCoercDeclaration.cmi +grafiteTypes.cmi: +nCicCoercDeclaration.cmi: grafiteTypes.cmi +grafiteEngine.cmi: grafiteTypes.cmi +grafiteTypes.cmo: grafiteTypes.cmi +grafiteTypes.cmx: grafiteTypes.cmi +nCicCoercDeclaration.cmo: grafiteTypes.cmi nCicCoercDeclaration.cmi +nCicCoercDeclaration.cmx: grafiteTypes.cmx nCicCoercDeclaration.cmi grafiteEngine.cmo: nCicCoercDeclaration.cmi grafiteTypes.cmi \ - grafiteEngine.cmi + grafiteEngine.cmi grafiteEngine.cmx: nCicCoercDeclaration.cmx grafiteTypes.cmx \ - grafiteEngine.cmi + grafiteEngine.cmi diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml index 630d6a6e3..bcbaa93ad 100644 --- a/matitaB/components/grafite_engine/grafiteEngine.ml +++ b/matitaB/components/grafite_engine/grafiteEngine.ml @@ -34,6 +34,8 @@ type options = { do_heavy_checks: bool ; } +let prerr_endline _ = () + let basic_eval_unification_hint (t,n) status = NCicUnifHint.add_user_provided_hint status t n ;; @@ -639,6 +641,65 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = (NCicEnvironment.get_universes status)))) status itl | _ -> status in + let status = match nobj with + NCic.Inductive (is_ind,leftno,itl,_) -> + (* first leibniz *) + let status' = List.fold_left + (fun status it -> + let _,ind_name,ty,cl = it in + let status = status#set_ng_mode `ProofMode in + try + prerr_endline ("creazione discriminatore per " ^ ind_name); + (let status,invobj = + NDestructTac.mk_discriminator ~use_jmeq:false + (ind_name ^ "_discr") + it leftno status status#baseuri in + let _,_,menv,_,_ = invobj in + (match menv with + [] -> eval_ncommand ~include_paths opts status + ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false)) + | _ -> status)) + (* XXX *) + with + | NDestructTac.ConstructorTooBig k -> + prerr_endline (Printf.sprintf + "unable to generate leibniz discrimination principle (constructor %s too big)" + k); + HLog.warn (Printf.sprintf + "unable to generate leibniz discrimination principle (constructor %s too big)" + k); + let status = status#set_ng_mode `CommandMode in status + | _ -> + prerr_endline "error in generating discrimination principle"; + (*HLog.warn "error in generating discrimination principle"; *) + let status = status#set_ng_mode `CommandMode in + status) + status itl + in + (* then JMeq *) + List.fold_left + (fun status it -> + let _,ind_name,ty,cl = it in + let status = status#set_ng_mode `ProofMode in + try + prerr_endline ("creazione discriminatore per " ^ ind_name); + (let status,invobj = + NDestructTac.mk_discriminator ~use_jmeq:true + (ind_name ^ "_jmdiscr") + it leftno status status#baseuri in + let _,_,menv,_,_ = invobj in + (match menv with + [] -> eval_ncommand ~include_paths opts status + ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false)) + | _ -> status)) + (* XXX *) + with _ -> (*HLog.warn "error in generating discrimination principle"; *) + prerr_endline "error in generating discrimination principle"; + let status = status#set_ng_mode `CommandMode in + status) + status' itl + | _ -> status + in let coercions = match obj with _,_,_,_,NCic.Inductive @@ -832,7 +893,8 @@ let rec eval_executable ~include_paths opts status (text,prefix_len,ex) = match ex with | GrafiteAst.NTactic (_(*loc*), tacl) -> if status#ng_mode <> `ProofMode then - raise (GrafiteTypes.Command_error "Not in proof mode") + (prerr_endline ("not in proof mode 2: " ^ GrafiteAstPp.pp_executable status ~map_unicode_to_tex:false ex); + raise (GrafiteTypes.Command_error "Not in proof mode")) else let status = List.fold_left diff --git a/matitaB/components/grafite_parser/.depend b/matitaB/components/grafite_parser/.depend index e5cd5f2b3..5142da1bf 100644 --- a/matitaB/components/grafite_parser/.depend +++ b/matitaB/components/grafite_parser/.depend @@ -1,6 +1,6 @@ -grafiteParser.cmi: -print_grammar.cmi: grafiteParser.cmi -grafiteParser.cmo: grafiteParser.cmi -grafiteParser.cmx: grafiteParser.cmi -print_grammar.cmo: print_grammar.cmi -print_grammar.cmx: print_grammar.cmi +grafiteParser.cmi: +print_grammar.cmi: grafiteParser.cmi +grafiteParser.cmo: grafiteParser.cmi +grafiteParser.cmx: grafiteParser.cmi +print_grammar.cmo: print_grammar.cmi +print_grammar.cmx: print_grammar.cmi diff --git a/matitaB/components/grafite_parser/print_grammar.ml b/matitaB/components/grafite_parser/print_grammar.ml index 5bc87f247..6bcc14687 100644 --- a/matitaB/components/grafite_parser/print_grammar.ml +++ b/matitaB/components/grafite_parser/print_grammar.ml @@ -87,7 +87,7 @@ and is_symbol_dummy = function | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt | Snterm e | Snterml (e, _) -> is_entry_dummy e | Slist1 x | Slist0 x -> is_symbol_dummy x - | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y + | Slist1sep (x,y,_) | Slist0sep (x,y,_) -> is_symbol_dummy x && is_symbol_dummy y | Sopt x -> is_symbol_dummy x | Sself | Snext -> false | Stree t -> is_tree_dummy t @@ -186,7 +186,7 @@ let visit_description desc fmt self = let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "@]} @ "; todo - | Slist0sep (symbol,sep) -> + | Slist0sep (symbol,sep,_) -> Format.fprintf fmt "[@[ "; let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "{@[ "; @@ -200,7 +200,7 @@ let visit_description desc fmt self = let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "@]}+ @ "; todo - | Slist1sep (symbol,sep) -> + | Slist1sep (symbol,sep,_) -> let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "{@[ "; let todo = visit_symbol sep todo is_son in diff --git a/matitaB/components/library/.depend b/matitaB/components/library/.depend index edb2abe95..28703386a 100644 --- a/matitaB/components/library/.depend +++ b/matitaB/components/library/.depend @@ -1,9 +1,9 @@ -librarian.cmi: -libraryMisc.cmi: -libraryClean.cmi: -librarian.cmo: librarian.cmi -librarian.cmx: librarian.cmi -libraryMisc.cmo: libraryMisc.cmi -libraryMisc.cmx: libraryMisc.cmi -libraryClean.cmo: libraryClean.cmi -libraryClean.cmx: libraryClean.cmi +librarian.cmi: +libraryMisc.cmi: +libraryClean.cmi: +librarian.cmo: librarian.cmi +librarian.cmx: librarian.cmi +libraryMisc.cmo: libraryMisc.cmi +libraryMisc.cmx: libraryMisc.cmi +libraryClean.cmo: libraryClean.cmi +libraryClean.cmx: libraryClean.cmi diff --git a/matitaB/components/logger/.depend b/matitaB/components/logger/.depend index dfb4400ff..1c8ec5b7c 100644 --- a/matitaB/components/logger/.depend +++ b/matitaB/components/logger/.depend @@ -1,3 +1,3 @@ -helmLogger.cmi: -helmLogger.cmo: helmLogger.cmi -helmLogger.cmx: helmLogger.cmi +helmLogger.cmi: +helmLogger.cmo: helmLogger.cmi +helmLogger.cmx: helmLogger.cmi diff --git a/matitaB/components/ng_cic_content/.depend b/matitaB/components/ng_cic_content/.depend index fd1b831b9..b1a499fd3 100644 --- a/matitaB/components/ng_cic_content/.depend +++ b/matitaB/components/ng_cic_content/.depend @@ -1,6 +1,6 @@ -ncic2astMatcher.cmi: -interpretations.cmi: -ncic2astMatcher.cmo: ncic2astMatcher.cmi -ncic2astMatcher.cmx: ncic2astMatcher.cmi -interpretations.cmo: ncic2astMatcher.cmi interpretations.cmi -interpretations.cmx: ncic2astMatcher.cmx interpretations.cmi +ncic2astMatcher.cmi: +interpretations.cmi: +ncic2astMatcher.cmo: ncic2astMatcher.cmi +ncic2astMatcher.cmx: ncic2astMatcher.cmi +interpretations.cmo: ncic2astMatcher.cmi interpretations.cmi +interpretations.cmx: ncic2astMatcher.cmx interpretations.cmi diff --git a/matitaB/components/ng_disambiguation/.depend b/matitaB/components/ng_disambiguation/.depend index 0810bc8be..d5306074a 100644 --- a/matitaB/components/ng_disambiguation/.depend +++ b/matitaB/components/ng_disambiguation/.depend @@ -1,14 +1,14 @@ -nnumber_notation.cmi: -disambiguateChoices.cmi: -nCicDisambiguate.cmi: -grafiteDisambiguate.cmi: -nnumber_notation.cmo: nnumber_notation.cmi -nnumber_notation.cmx: nnumber_notation.cmi -disambiguateChoices.cmo: nnumber_notation.cmi disambiguateChoices.cmi -disambiguateChoices.cmx: nnumber_notation.cmx disambiguateChoices.cmi -nCicDisambiguate.cmo: nCicDisambiguate.cmi -nCicDisambiguate.cmx: nCicDisambiguate.cmi +nnumber_notation.cmi: +disambiguateChoices.cmi: +nCicDisambiguate.cmi: +grafiteDisambiguate.cmi: +nnumber_notation.cmo: nnumber_notation.cmi +nnumber_notation.cmx: nnumber_notation.cmi +disambiguateChoices.cmo: nnumber_notation.cmi disambiguateChoices.cmi +disambiguateChoices.cmx: nnumber_notation.cmx disambiguateChoices.cmi +nCicDisambiguate.cmo: nCicDisambiguate.cmi +nCicDisambiguate.cmx: nCicDisambiguate.cmi grafiteDisambiguate.cmo: nCicDisambiguate.cmi disambiguateChoices.cmi \ - grafiteDisambiguate.cmi + grafiteDisambiguate.cmi grafiteDisambiguate.cmx: nCicDisambiguate.cmx disambiguateChoices.cmx \ - grafiteDisambiguate.cmi + grafiteDisambiguate.cmi diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml index c39ac161d..162e172a4 100644 --- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml +++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml @@ -353,7 +353,7 @@ let disambiguate_nterm status expty context metasenv subst thing diff_term Stdpp.dummy_loc thing' ast) choices in raise (Ambiguous_input (find_diffs diffs)) - | Disambiguate.Disamb_failure (l,_) -> + | Disambiguate.Disamb_failure l -> raise (Error (List.map (clusterize (diff_term Stdpp.dummy_loc thing')) l)) | _ -> assert false ;; @@ -440,7 +440,7 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj as obj') = diff_obj Stdpp.dummy_loc obj ast) choices in raise (Ambiguous_input (find_diffs diffs)) - | Disambiguate.Disamb_failure (l,_) -> + | Disambiguate.Disamb_failure l -> raise (Error (List.map (clusterize (diff_obj Stdpp.dummy_loc obj)) l)) | _ -> assert false ;; diff --git a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml index ff6f70e94..c34a57315 100644 --- a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml +++ b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml @@ -654,8 +654,8 @@ let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library ~local_names | DisambiguateTypes.Symbol _ -> "SYM" | DisambiguateTypes.Num _ -> "NUM" in - prerr_endline (Printf.sprintf "lookup_choices of %s returns length %d" id - (List.length res)); + debug_print (lazy (Printf.sprintf "lookup_choices of %s returns length %d" id + (List.length res))); res with Not_found -> []) in diff --git a/matitaB/components/ng_kernel/.depend b/matitaB/components/ng_kernel/.depend index 0bf995539..a004d18af 100644 --- a/matitaB/components/ng_kernel/.depend +++ b/matitaB/components/ng_kernel/.depend @@ -1,41 +1,41 @@ -nUri.cmi: -nReference.cmi: nUri.cmi -nCicUtils.cmi: nCic.cmo -nCicSubstitution.cmi: nCic.cmo -nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmo -nCicReduction.cmi: nCic.cmo -nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmo -nCicUntrusted.cmi: nCic.cmo -nCicPp.cmi: nReference.cmi nCic.cmo -nCic.cmo: nUri.cmi nReference.cmi -nCic.cmx: nUri.cmx nReference.cmx -nUri.cmo: nUri.cmi -nUri.cmx: nUri.cmi -nReference.cmo: nUri.cmi nReference.cmi -nReference.cmx: nUri.cmx nReference.cmi -nCicUtils.cmo: nReference.cmi nCic.cmo nCicUtils.cmi -nCicUtils.cmx: nReference.cmx nCic.cmx nCicUtils.cmi +nUri.cmi: +nReference.cmi: nUri.cmi +nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmo +nCicUtils.cmi: nCicEnvironment.cmi nCic.cmo +nCicSubstitution.cmi: nCicEnvironment.cmi nCic.cmo +nCicReduction.cmi: nCicEnvironment.cmi nCic.cmo +nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCicEnvironment.cmi nCic.cmo +nCicUntrusted.cmi: nCicEnvironment.cmi nCic.cmo +nCicPp.cmi: nReference.cmi nCicEnvironment.cmi nCic.cmo +nCic.cmo: nUri.cmi nReference.cmi +nCic.cmx: nUri.cmx nReference.cmx +nUri.cmo: nUri.cmi +nUri.cmx: nUri.cmi +nReference.cmo: nUri.cmi nReference.cmi +nReference.cmx: nUri.cmx nReference.cmi +nCicEnvironment.cmo: nUri.cmi nReference.cmi nCic.cmo nCicEnvironment.cmi +nCicEnvironment.cmx: nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi +nCicUtils.cmo: nReference.cmi nCicEnvironment.cmi nCic.cmo nCicUtils.cmi +nCicUtils.cmx: nReference.cmx nCicEnvironment.cmx nCic.cmx nCicUtils.cmi nCicSubstitution.cmo: nReference.cmi nCicUtils.cmi nCic.cmo \ - nCicSubstitution.cmi + nCicSubstitution.cmi nCicSubstitution.cmx: nReference.cmx nCicUtils.cmx nCic.cmx \ - nCicSubstitution.cmi -nCicEnvironment.cmo: nUri.cmi nReference.cmi nCic.cmo nCicEnvironment.cmi -nCicEnvironment.cmx: nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi + nCicSubstitution.cmi nCicReduction.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ - nCicEnvironment.cmi nCic.cmo nCicReduction.cmi + nCicEnvironment.cmi nCic.cmo nCicReduction.cmi nCicReduction.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ - nCicEnvironment.cmx nCic.cmx nCicReduction.cmi + nCicEnvironment.cmx nCic.cmx nCicReduction.cmi nCicTypeChecker.cmo: nUri.cmi nReference.cmi nCicUtils.cmi \ nCicSubstitution.cmi nCicReduction.cmi nCicEnvironment.cmi nCic.cmo \ - nCicTypeChecker.cmi + nCicTypeChecker.cmi nCicTypeChecker.cmx: nUri.cmx nReference.cmx nCicUtils.cmx \ nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx nCic.cmx \ - nCicTypeChecker.cmi + nCicTypeChecker.cmi nCicUntrusted.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ - nCicReduction.cmi nCicEnvironment.cmi nCic.cmo nCicUntrusted.cmi + nCicReduction.cmi nCicEnvironment.cmi nCic.cmo nCicUntrusted.cmi nCicUntrusted.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ - nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi + nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \ - nCicEnvironment.cmi nCic.cmo nCicPp.cmi + nCicEnvironment.cmi nCic.cmo nCicPp.cmi nCicPp.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \ - nCicEnvironment.cmx nCic.cmx nCicPp.cmi + nCicEnvironment.cmx nCic.cmx nCicPp.cmi diff --git a/matitaB/components/ng_library/.depend b/matitaB/components/ng_library/.depend index 48127a325..b9e7731f9 100644 --- a/matitaB/components/ng_library/.depend +++ b/matitaB/components/ng_library/.depend @@ -1,3 +1,3 @@ -nCicLibrary.cmi: -nCicLibrary.cmo: nCicLibrary.cmi -nCicLibrary.cmx: nCicLibrary.cmi +nCicLibrary.cmi: +nCicLibrary.cmo: nCicLibrary.cmi +nCicLibrary.cmx: nCicLibrary.cmi diff --git a/matitaB/components/ng_library/nCicLibrary.ml b/matitaB/components/ng_library/nCicLibrary.ml index 201b5ac08..a7e35f427 100644 --- a/matitaB/components/ng_library/nCicLibrary.ml +++ b/matitaB/components/ng_library/nCicLibrary.ml @@ -16,6 +16,8 @@ exception IncludedFileNotCompiled of string * string let magic = 2;; +let prerr_endline _ = () + let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);; let refresh_uri_in_universe = @@ -79,7 +81,12 @@ let require_path path = let require0 user ~baseuri = require_path (ng_path_of_baseuri user baseuri) -let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";; +let db_path user = + let midpath = match user with + | None -> "" + | Some u -> "/" ^ u + in + Helm_registry.get "matita.basedir" ^ midpath ^ "/ng_db.ng";; type timestamp = [ `Obj of NUri.uri * NCic.obj @@ -89,17 +96,35 @@ type timestamp = let time0 = [],[];; +let global_aliases_db = ref [];; +let rev_includes_map_db = ref [];; + +let global_aliases u = + try List.assoc u !global_aliases_db + with Not_found -> + let db = ref [] in + global_aliases_db := (u,db)::!global_aliases_db; + db +;; + +let rev_includes_map u = + try List.assoc u !rev_includes_map_db + with Not_found -> + let db = ref NUri.UriMap.empty in + rev_includes_map_db := (u,db)::!rev_includes_map_db; + db +;; + let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps= - let global_aliases = ref [] in - let rev_includes_map = ref NUri.UriMap.empty in - let store_db () = - let ch = open_out (db_path ()) in - Marshal.to_channel ch (magic,(!global_aliases,!rev_includes_map)) []; + let store_db user = + let ch = open_out (db_path user) in + Marshal.to_channel ch (magic,(!(global_aliases user),!(rev_includes_map user))) []; close_out ch in - let load_db () = + let load_db user = HExtlib.mkdir (Helm_registry.get "matita.basedir"); + if user <> None then HExtlib.mkdir ((Helm_registry.get "matita.basedir") ^ "/" ^ HExtlib.unopt user); try - let ga,im = require_path (db_path ()) in + let ga,im = require_path (db_path user) in let ga = List.map (fun (uri,name,NReference.Ref (uri2,spec)) -> @@ -110,13 +135,13 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps= (fun u l im -> NUri.UriMap.add (refresh_uri u) (List.map refresh_uri l) im ) im NUri.UriMap.empty in - global_aliases := ga; - rev_includes_map := im + global_aliases user := ga; + rev_includes_map user := im with Sys_error _ -> () in - let get_deps u = + let get_deps user u = let get_deps_one_step u = - try NUri.UriMap.find u !rev_includes_map with Not_found -> [] in + try NUri.UriMap.find u !(rev_includes_map user) with Not_found -> [] in let rec aux res = function [] -> res @@ -127,19 +152,19 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps= aux (he::res) (get_deps_one_step he @ tl) in aux [] [u] in - let remove_deps u = - rev_includes_map := NUri.UriMap.remove u !rev_includes_map; - rev_includes_map := + let remove_deps user u = + rev_includes_map user := NUri.UriMap.remove u !(rev_includes_map user); + rev_includes_map user := NUri.UriMap.map - (fun l -> List.filter (fun uri -> not (NUri.eq u uri)) l) !rev_includes_map; - store_db () + (fun l -> List.filter (fun uri -> not (NUri.eq u uri)) l) !(rev_includes_map user); + store_db user in load_db, - (fun ga -> global_aliases := ga; store_db ()), - (fun () -> !global_aliases), - (fun u l -> - rev_includes_map := NUri.UriMap.add u (l @ get_deps u) !rev_includes_map; - store_db ()), + (fun user ga -> global_aliases user := ga; store_db user), + (fun user -> !(global_aliases user)), + (fun user u l -> + rev_includes_map user := NUri.UriMap.add u (l @ get_deps user u) !(rev_includes_map user); + store_db user), get_deps, remove_deps ;; @@ -173,6 +198,11 @@ class virtual status uid = val timestamp = (time0 : timestamp) method timestamp = timestamp + method print_timestamp () = + prerr_endline ("length(lib_db.storage) = " ^ + string_of_int (List.length !(lib_db.storage))); + prerr_endline ("length(timestamp.storage) = " ^ + string_of_int (List.length (fst timestamp))); method set_timestamp v = {< timestamp = v >} method set_lib_db v = {< lib_db = v >} method set_lib_status : 's.#g_status as 's -> 'self @@ -185,6 +215,8 @@ let reset_timestamp st = ;; let time_travel0 st (sto,ali) = + prerr_endline ("length of lib_db.storage = " ^ (string_of_int (List.length !(st#lib_db.storage)))); + prerr_endline ("length of sto = " ^ (string_of_int (List.length sto))); let diff_len = List.length !(st#lib_db.storage) - List.length sto in let to_be_deleted,_ = HExtlib.split_nth diff_len !(st#lib_db.storage) in if List.length to_be_deleted > 0 then @@ -247,8 +279,8 @@ module type SerializerType = end module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status - val set: dumpable_s -> dumpable_status -> dumpable_s (*val user : dumpable_s -> - string option*) end) = + val set: dumpable_s -> dumpable_status -> dumpable_s val user : dumpable_s -> + string option end) = struct type dumpable_status = D.dumpable_s type 'a register_type = @@ -296,8 +328,9 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status close_out ch | `Constr _ -> () ) !((D.get status)#lib_db.storage); - set_global_aliases (!((D.get status)#lib_db.local_aliases) @ get_global_aliases ()); - List.iter (fun u -> add_deps u [baseuri]) (D.get status)#dump.includes; + let user = D.user status in + set_global_aliases user (!((D.get status)#lib_db.local_aliases) @ get_global_aliases user); + List.iter (fun u -> add_deps (D.user status) u [baseuri]) (D.get status)#dump.includes; reset_timestamp (D.get status) let require2 ~baseuri ~alias_only status = @@ -359,7 +392,7 @@ let resolve st name = try HExtlib.filter_map (fun (_,name',nref) -> if name'=name then Some nref else None) - (!(st#lib_db.local_aliases) @ get_global_aliases ()) + (!(st#lib_db.local_aliases) @ get_global_aliases st#user) with Not_found -> (prerr_endline ("can't resolve object " ^ name); diff --git a/matitaB/components/ng_library/nCicLibrary.mli b/matitaB/components/ng_library/nCicLibrary.mli index b8453267a..badf17884 100644 --- a/matitaB/components/ng_library/nCicLibrary.mli +++ b/matitaB/components/ng_library/nCicLibrary.mli @@ -31,6 +31,7 @@ class virtual status : inherit g_status method lib_db: db method timestamp: timestamp + method print_timestamp : unit -> unit method set_timestamp: timestamp -> 'self method set_lib_db: db -> 'self method set_lib_status: #g_status -> 'self @@ -49,7 +50,7 @@ val get_obj: #NCic.status -> NUri.uri -> NCic.obj (* changes the current timesta val time_travel: #status -> unit -val init: unit -> unit +val init: string option -> unit type obj type dump diff --git a/matitaB/components/ng_paramodulation/.depend b/matitaB/components/ng_paramodulation/.depend index 2e31be0ec..f6eae06d6 100644 --- a/matitaB/components/ng_paramodulation/.depend +++ b/matitaB/components/ng_paramodulation/.depend @@ -1,45 +1,45 @@ -terms.cmi: -pp.cmi: terms.cmi -foSubst.cmi: terms.cmi -orderings.cmi: terms.cmi -foUtils.cmi: terms.cmi orderings.cmi -foUnif.cmi: terms.cmi orderings.cmi -index.cmi: terms.cmi orderings.cmi -superposition.cmi: terms.cmi orderings.cmi index.cmi -stats.cmi: terms.cmi orderings.cmi -paramod.cmi: terms.cmi orderings.cmi -nCicBlob.cmi: terms.cmi -nCicProof.cmi: terms.cmi -nCicParamod.cmi: -terms.cmo: terms.cmi -terms.cmx: terms.cmi -pp.cmo: terms.cmi pp.cmi -pp.cmx: terms.cmx pp.cmi -foSubst.cmo: terms.cmi foSubst.cmi -foSubst.cmx: terms.cmx foSubst.cmi -orderings.cmo: terms.cmi pp.cmi foSubst.cmi orderings.cmi -orderings.cmx: terms.cmx pp.cmx foSubst.cmx orderings.cmi -foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi -foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi -foUnif.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi -foUnif.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi -index.cmo: terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi index.cmi -index.cmx: terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx index.cmi +terms.cmi: +pp.cmi: terms.cmi +foSubst.cmi: terms.cmi +orderings.cmi: terms.cmi +foUtils.cmi: terms.cmi orderings.cmi +foUnif.cmi: terms.cmi orderings.cmi +index.cmi: terms.cmi orderings.cmi +superposition.cmi: terms.cmi orderings.cmi index.cmi +stats.cmi: terms.cmi orderings.cmi +paramod.cmi: terms.cmi orderings.cmi +nCicBlob.cmi: terms.cmi +nCicProof.cmi: terms.cmi +nCicParamod.cmi: +terms.cmo: terms.cmi +terms.cmx: terms.cmi +pp.cmo: terms.cmi pp.cmi +pp.cmx: terms.cmx pp.cmi +foSubst.cmo: terms.cmi foSubst.cmi +foSubst.cmx: terms.cmx foSubst.cmi +orderings.cmo: terms.cmi pp.cmi foSubst.cmi orderings.cmi +orderings.cmx: terms.cmx pp.cmx foSubst.cmx orderings.cmi +foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi +foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi +foUnif.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi +foUnif.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi +index.cmo: terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi index.cmi +index.cmx: terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx index.cmi superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \ - foUnif.cmi foSubst.cmi superposition.cmi + foUnif.cmi foSubst.cmi superposition.cmi superposition.cmx: terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \ - foUnif.cmx foSubst.cmx superposition.cmi -stats.cmo: terms.cmi stats.cmi -stats.cmx: terms.cmx stats.cmi + foUnif.cmx foSubst.cmx superposition.cmi +stats.cmo: terms.cmi stats.cmi +stats.cmx: terms.cmx stats.cmi paramod.cmo: terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \ - foUtils.cmi foUnif.cmi paramod.cmi + foUtils.cmi foUnif.cmi paramod.cmi paramod.cmx: terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \ - foUtils.cmx foUnif.cmx paramod.cmi -nCicBlob.cmo: terms.cmi foUtils.cmi nCicBlob.cmi -nCicBlob.cmx: terms.cmx foUtils.cmx nCicBlob.cmi -nCicProof.cmo: terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi -nCicProof.cmx: terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi + foUtils.cmx foUnif.cmx paramod.cmi +nCicBlob.cmo: terms.cmi foUtils.cmi nCicBlob.cmi +nCicBlob.cmx: terms.cmx foUtils.cmx nCicBlob.cmi +nCicProof.cmo: terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi +nCicProof.cmx: terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi nCicParamod.cmo: terms.cmi pp.cmi paramod.cmi orderings.cmi nCicProof.cmi \ - nCicBlob.cmi nCicParamod.cmi + nCicBlob.cmi nCicParamod.cmi nCicParamod.cmx: terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \ - nCicBlob.cmx nCicParamod.cmi + nCicBlob.cmx nCicParamod.cmi diff --git a/matitaB/components/ng_refiner/.depend b/matitaB/components/ng_refiner/.depend index 2633e1aba..5e055ecdc 100644 --- a/matitaB/components/ng_refiner/.depend +++ b/matitaB/components/ng_refiner/.depend @@ -1,25 +1,25 @@ -nDiscriminationTree.cmi: -nCicMetaSubst.cmi: -nCicUnifHint.cmi: -nCicCoercion.cmi: nCicUnifHint.cmi -nCicRefineUtil.cmi: -nCicUnification.cmi: nCicCoercion.cmi -nCicRefiner.cmi: nCicCoercion.cmi -nDiscriminationTree.cmo: nDiscriminationTree.cmi -nDiscriminationTree.cmx: nDiscriminationTree.cmi -nCicMetaSubst.cmo: nCicMetaSubst.cmi -nCicMetaSubst.cmx: nCicMetaSubst.cmi -nCicUnifHint.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicUnifHint.cmi -nCicUnifHint.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicUnifHint.cmi +nDiscriminationTree.cmi: +nCicMetaSubst.cmi: +nCicUnifHint.cmi: +nCicCoercion.cmi: nCicUnifHint.cmi +nCicRefineUtil.cmi: +nCicUnification.cmi: nCicCoercion.cmi +nCicRefiner.cmi: nCicCoercion.cmi +nDiscriminationTree.cmo: nDiscriminationTree.cmi +nDiscriminationTree.cmx: nDiscriminationTree.cmi +nCicMetaSubst.cmo: nCicMetaSubst.cmi +nCicMetaSubst.cmx: nCicMetaSubst.cmi +nCicUnifHint.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicUnifHint.cmi +nCicUnifHint.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicUnifHint.cmi nCicCoercion.cmo: nDiscriminationTree.cmi nCicUnifHint.cmi nCicMetaSubst.cmi \ - nCicCoercion.cmi + nCicCoercion.cmi nCicCoercion.cmx: nDiscriminationTree.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \ - nCicCoercion.cmi -nCicRefineUtil.cmo: nCicMetaSubst.cmi nCicRefineUtil.cmi -nCicRefineUtil.cmx: nCicMetaSubst.cmx nCicRefineUtil.cmi -nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi -nCicUnification.cmx: nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi + nCicCoercion.cmi +nCicRefineUtil.cmo: nCicMetaSubst.cmi nCicRefineUtil.cmi +nCicRefineUtil.cmx: nCicMetaSubst.cmx nCicRefineUtil.cmi +nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi +nCicUnification.cmx: nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi nCicRefiner.cmo: nCicUnification.cmi nCicRefineUtil.cmi nCicMetaSubst.cmi \ - nCicCoercion.cmi nCicRefiner.cmi + nCicCoercion.cmi nCicRefiner.cmi nCicRefiner.cmx: nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \ - nCicCoercion.cmx nCicRefiner.cmi + nCicCoercion.cmx nCicRefiner.cmi diff --git a/matitaB/components/ng_refiner/nCicRefiner.ml b/matitaB/components/ng_refiner/nCicRefiner.ml index 7cdeb875e..4f8be9c53 100644 --- a/matitaB/components/ng_refiner/nCicRefiner.ml +++ b/matitaB/components/ng_refiner/nCicRefiner.ml @@ -506,6 +506,11 @@ and try_coercions status (* we try with a coercion *) let rec first exc = function | [] -> + let expty = + match expty with + `Type expty -> status#ppterm ~metasenv ~subst ~context expty + | `Sort -> "[[sort]]" + | `Prod -> "[[prod]]" in pp (lazy "WWW: no more coercions!"); raise (wrap_exc (lazy (localise orig_t, Printf.sprintf "The term\n%s\nhas type\n%s\nbut is here used with type\n%s" @@ -886,7 +891,7 @@ and try_coercions status `Type expty -> expty | `Sort -> NCic.Sort (NCic.Type - (match NCicEnvironment.get_universes () with + (match NCicEnvironment.get_universes status with | x::_ -> x | _ -> assert false)) | `Prod -> NCic.Prod ("_",NCic.Implicit `Type,NCic.Implicit `Type) @@ -1260,7 +1265,7 @@ let typeof_obj NCicReduction.whd status ~subst [] ty_sort with (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) -> - if not (NCicEnvironment.universe_leq u1 u2) then + if not (NCicEnvironment.universe_leq status u1 u2) then raise (RefineFailure (lazy(localise te, "The type " ^ diff --git a/matitaB/components/ng_refiner/nCicUnification.ml b/matitaB/components/ng_refiner/nCicUnification.ml index d45b14fc9..57bafe0a3 100644 --- a/matitaB/components/ng_refiner/nCicUnification.ml +++ b/matitaB/components/ng_refiner/nCicUnification.ml @@ -590,7 +590,7 @@ and fo_unif0 during_delift status swap test_eq_only metasenv subst context (norm let tym = NCicSubstitution.subst_meta status lc tym in match tyn,tym with NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 -> - NCicEnvironment.universe_lt u1 u2 + NCicEnvironment.universe_lt status u1 u2 | _,_ -> false -> instantiate status test_eq_only metasenv subst context m lc' (NCicReduction.head_beta_reduce status ~subst t1) (not swap) diff --git a/matitaB/components/ng_tactics/.depend b/matitaB/components/ng_tactics/.depend index 47f203f0a..4c247cb5d 100644 --- a/matitaB/components/ng_tactics/.depend +++ b/matitaB/components/ng_tactics/.depend @@ -1,28 +1,28 @@ -continuationals.cmi: -nCicTacReduction.cmi: -nTacStatus.cmi: continuationals.cmi -nCicElim.cmi: -nTactics.cmi: nTacStatus.cmi -nnAuto.cmi: nTacStatus.cmi -nDestructTac.cmi: nTacStatus.cmi -nInversion.cmi: nTacStatus.cmi -continuationals.cmo: continuationals.cmi -continuationals.cmx: continuationals.cmi -nCicTacReduction.cmo: nCicTacReduction.cmi -nCicTacReduction.cmx: nCicTacReduction.cmi -nTacStatus.cmo: nCicTacReduction.cmi continuationals.cmi nTacStatus.cmi -nTacStatus.cmx: nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi -nCicElim.cmo: nCicElim.cmi -nCicElim.cmx: nCicElim.cmi -nTactics.cmo: nTacStatus.cmi nCicElim.cmi continuationals.cmi nTactics.cmi -nTactics.cmx: nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi +continuationals.cmi: +nCicTacReduction.cmi: +nTacStatus.cmi: continuationals.cmi +nCicElim.cmi: +nTactics.cmi: nTacStatus.cmi +nnAuto.cmi: nTacStatus.cmi +nDestructTac.cmi: nTacStatus.cmi +nInversion.cmi: nTacStatus.cmi +continuationals.cmo: continuationals.cmi +continuationals.cmx: continuationals.cmi +nCicTacReduction.cmo: nCicTacReduction.cmi +nCicTacReduction.cmx: nCicTacReduction.cmi +nTacStatus.cmo: nCicTacReduction.cmi continuationals.cmi nTacStatus.cmi +nTacStatus.cmx: nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi +nCicElim.cmo: nCicElim.cmi +nCicElim.cmx: nCicElim.cmi +nTactics.cmo: nTacStatus.cmi nCicElim.cmi continuationals.cmi nTactics.cmi +nTactics.cmx: nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi nnAuto.cmo: nTactics.cmi nTacStatus.cmi nCicTacReduction.cmi \ - continuationals.cmi nnAuto.cmi + continuationals.cmi nnAuto.cmi nnAuto.cmx: nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \ - continuationals.cmx nnAuto.cmi + continuationals.cmx nnAuto.cmi nDestructTac.cmo: nTactics.cmi nTacStatus.cmi continuationals.cmi \ - nDestructTac.cmi + nDestructTac.cmi nDestructTac.cmx: nTactics.cmx nTacStatus.cmx continuationals.cmx \ - nDestructTac.cmi -nInversion.cmo: nTactics.cmi nCicElim.cmi continuationals.cmi nInversion.cmi -nInversion.cmx: nTactics.cmx nCicElim.cmx continuationals.cmx nInversion.cmi + nDestructTac.cmi +nInversion.cmo: nTactics.cmi nCicElim.cmi continuationals.cmi nInversion.cmi +nInversion.cmx: nTactics.cmx nCicElim.cmx continuationals.cmx nInversion.cmi diff --git a/matitaB/components/ng_tactics/nDestructTac.ml b/matitaB/components/ng_tactics/nDestructTac.ml index dcd774994..d50a98f08 100644 --- a/matitaB/components/ng_tactics/nDestructTac.ml +++ b/matitaB/components/ng_tactics/nDestructTac.ml @@ -28,7 +28,7 @@ open NTacStatus open Continuationals.Stack -let debug = false +let debug = true let pp = if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ()) @@ -638,13 +638,12 @@ let select_eq ctx acc domain status goal = let tagged_intro_tac curtag name = match curtag with - | _ -> NTactics.intro_tac name -(* | `Eq use_jmeq -> + | `Eq false -> NTactics.block_tac [ NTactics.intro_tac name ; NTactics.reduce_tac - ~reduction:(`Whd true) ~where:((if use_jmeq then hp_pattern_jm else - hp_pattern) name) ] *) + ~reduction:(`Whd true) ~where:(hp_pattern name) ] + | _ -> NTactics.intro_tac name (* status in distribute_tac (fun s g -> diff --git a/matitaB/components/registry/.depend b/matitaB/components/registry/.depend index 40c03891a..19a1fd325 100644 --- a/matitaB/components/registry/.depend +++ b/matitaB/components/registry/.depend @@ -1,3 +1,3 @@ -helm_registry.cmi: -helm_registry.cmo: helm_registry.cmi -helm_registry.cmx: helm_registry.cmi +helm_registry.cmi: +helm_registry.cmo: helm_registry.cmi +helm_registry.cmx: helm_registry.cmi diff --git a/matitaB/components/syntax_extensions/.depend b/matitaB/components/syntax_extensions/.depend index 25e67131f..119f13093 100644 --- a/matitaB/components/syntax_extensions/.depend +++ b/matitaB/components/syntax_extensions/.depend @@ -1,5 +1,5 @@ -utf8Macro.cmi: -utf8MacroTable.cmo: -utf8MacroTable.cmx: -utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi -utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi +utf8Macro.cmi: +utf8MacroTable.cmo: +utf8MacroTable.cmx: +utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi +utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi diff --git a/matitaB/components/syntax_extensions/make_table.ml b/matitaB/components/syntax_extensions/make_table.ml index 0e9a9ac12..84787e896 100644 --- a/matitaB/components/syntax_extensions/make_table.ml +++ b/matitaB/components/syntax_extensions/make_table.ml @@ -95,7 +95,7 @@ let main () = Hashtbl.iter (fun macro utf8 -> let hescape s = - String.escaped (Netencoding.Html.encode ~in_enc:`Enc_utf8 () s) in + String.escaped (Netencoding.Html.encode ~prefer_name:false ~in_enc:`Enc_utf8 () s) in fprintf oc " \"%s\", \"%s\";\n" macro (String.escaped utf8); fprintf oc_doc "\\%s %s\n" macro utf8; fprintf oc_js "macro2utf8[\"%s\"] = \"%s\";\n" diff --git a/matitaB/components/thread/.depend b/matitaB/components/thread/.depend index 6616a03d0..e25145b8b 100644 --- a/matitaB/components/thread/.depend +++ b/matitaB/components/thread/.depend @@ -1,6 +1,6 @@ -threadSafe.cmi: -extThread.cmi: -threadSafe.cmo: threadSafe.cmi -threadSafe.cmx: threadSafe.cmi -extThread.cmo: extThread.cmi -extThread.cmx: extThread.cmi +threadSafe.cmi: +extThread.cmi: +threadSafe.cmo: threadSafe.cmi +threadSafe.cmx: threadSafe.cmi +extThread.cmo: extThread.cmi +extThread.cmx: extThread.cmi diff --git a/matitaB/components/xml/.depend b/matitaB/components/xml/.depend index e7e7ffbd7..eda62779f 100644 --- a/matitaB/components/xml/.depend +++ b/matitaB/components/xml/.depend @@ -1,6 +1,6 @@ -xml.cmi: -xmlPushParser.cmi: -xml.cmo: xml.cmi -xml.cmx: xml.cmi -xmlPushParser.cmo: xmlPushParser.cmi -xmlPushParser.cmx: xmlPushParser.cmi +xml.cmi: +xmlPushParser.cmi: +xml.cmo: xml.cmi +xml.cmx: xml.cmi +xmlPushParser.cmo: xmlPushParser.cmi +xmlPushParser.cmx: xmlPushParser.cmi diff --git a/matitaB/matita/html/register.html b/matitaB/matita/html/register.html new file mode 100755 index 000000000..3d04c2f0d --- /dev/null +++ b/matitaB/matita/html/register.html @@ -0,0 +1,27 @@ + + + + + + + +

Matita web: Register new user

+
+ + + + + + + + + +
User id:
Password:
+ + + +
+ + + + diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml index 83eb235fb..14716e2b6 100644 --- a/matitaB/matita/matitaEngine.ml +++ b/matitaB/matita/matitaEngine.ml @@ -156,12 +156,14 @@ and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status match cont with | None -> asserted, true, status | Some (asserted,ast) -> + (* pp_ast_statement status ast; *) cb status ast; let status = eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in asserted, false, status with exn when not matita_debug -> + prerr_endline ("EnrichedWithStatus: " ^ Printexc.to_string exn); raise (EnrichedWithStatus (exn, status)) in if stop then asserted,status else loop asserted status @@ -172,6 +174,7 @@ and compile ~compiling ~asserted ~include_paths ~outch ?uid fname = if List.mem fname compiling then raise (CircularDependency fname); let compiling = fname::compiling in let matita_debug = Helm_registry.get_bool "matita.debug" in + let matita_debug = true in let root,baseuri,fname,_tgt = Librarian.baseuri_of_script ~include_paths fname in if Http_getter_storage.is_read_only baseuri then assert false; @@ -211,6 +214,7 @@ and compile ~compiling ~asserted ~include_paths ~outch ?uid fname = (Filename.dirname (Http_getter.filename ~local:true ~writable:true (baseuri ^ "foo.con"))); + prerr_endline ("trying to compile " ^ fname); let buf = GrafiteParser.parsable_statement status (Ulexing.from_utf8_channel (open_in fname)) @@ -221,6 +225,7 @@ and compile ~compiling ~asserted ~include_paths ~outch ?uid fname = in let asserted, status = eval_from_stream ~compiling ~asserted ~include_paths status buf print_cb in + prerr_endline ("end compile of " ^ fname); let elapsed = Unix.time () -. time in (if Helm_registry.get_bool "matita.moo" then begin GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) @@ -237,12 +242,13 @@ and compile ~compiling ~asserted ~include_paths ~outch ?uid fname = HLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); pp_times fname true big_bang big_bang_u big_bang_s; - (* XXX: update script -- currently to stdout *) + prerr_endline ("now generating disambiguated script for " ^ fname); let origbuf = Ulexing.from_utf8_channel (open_in fname) in let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in let outstr = ref "" in ignore (SmallLexer.mk_small_printer interpr outstr origbuf); Printf.fprintf outch "%s" !outstr; + prerr_endline ("returning after compilation of " ^ fname); asserted (* MATITA 1.0: debbo fare time_travel sulla ng_library? LexiconSync.time_travel -- 2.39.2