-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
-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
module Ast = NotationPt
module Env = NotationEnv
+let prerr_endline _ = ()
+
exception Parse_error of string
exception Level_not_found of int
| 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),
-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
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
* 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 =
(*| 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;;
"\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))))
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)
;;
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
-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
-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
-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
-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
do_heavy_checks: bool ;
}
+let prerr_endline _ = ()
+
let basic_eval_unification_hint (t,n) status =
NCicUnifHint.add_user_provided_hint status t n
;;
(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
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
-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
| 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
let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "@]} @ ";
todo
- | Slist0sep (symbol,sep) ->
+ | Slist0sep (symbol,sep,_) ->
Format.fprintf fmt "[@[<hov2> ";
let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "{@[<hov2> ";
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 "{@[<hov2> ";
let todo = visit_symbol sep todo is_son in
-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
-helmLogger.cmi:
-helmLogger.cmo: helmLogger.cmi
-helmLogger.cmx: helmLogger.cmi
+helmLogger.cmi:
+helmLogger.cmo: helmLogger.cmi
+helmLogger.cmx: helmLogger.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
+ncic2astMatcher.cmi:
+interpretations.cmi:
+ncic2astMatcher.cmo: ncic2astMatcher.cmi
+ncic2astMatcher.cmx: ncic2astMatcher.cmi
+interpretations.cmo: ncic2astMatcher.cmi interpretations.cmi
+interpretations.cmx: ncic2astMatcher.cmx interpretations.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
+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_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
;;
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
;;
| 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
-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
-nCicLibrary.cmi:
-nCicLibrary.cmo: nCicLibrary.cmi
-nCicLibrary.cmx: nCicLibrary.cmi
+nCicLibrary.cmi:
+nCicLibrary.cmo: nCicLibrary.cmi
+nCicLibrary.cmx: nCicLibrary.cmi
let magic = 2;;
+let prerr_endline _ = ()
+
let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);;
let refresh_uri_in_universe =
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
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)) ->
(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
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
;;
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
;;
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
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 =
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 =
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);
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
val time_travel: #status -> unit
-val init: unit -> unit
+val init: string option -> unit
type obj
type dump
-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
-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
(* 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"
`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)
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 " ^
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)
-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
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 _ -> ())
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 ->
-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
-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
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"
-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
-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
--- /dev/null
+<html>
+<head>
+</head>
+
+<head></head>
+
+<body>
+<H1>Matita web: Register new user</H1>
+<FORM action="register" method="post">
+<table>
+ <tr>
+ <td>User id: </td>
+ <td><INPUT type="TEXT" name="userid"></td>
+ </tr>
+ <tr>
+ <td>Password: </td>
+ <td><INPUT type="PASSWORD" name="password"></td>
+ </tr>
+</table>
+
+<INPUT type="SUBMIT" value="Register">
+<INPUT type="RESET" value="Reset">
+</FORM>
+
+</body>
+</html>
+
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
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;
(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))
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)
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
projects / helm.git / commitdiff