(* $Id$ *)
-exception Drop
(* mo file name, ma file name *)
-exception IncludedFileNotCompiled of string * string
-exception Macro of
- GrafiteAst.loc *
- (Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro)
exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
type 'a disambiguator_input = string * int * 'a
do_heavy_checks: bool ;
}
-let concat_nuris uris nuris =
- match uris,nuris with
- | `New uris, `New nuris -> `New (nuris@uris)
- | _ -> assert false
-;;
-(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
- * names as long as they are available, then it fallbacks to name generation
- * using FreshNamesGenerator module *)
-let namer_of names =
- let len = List.length names in
- let count = ref 0 in
- fun metasenv context name ~typ ->
- if !count < len then begin
- let name = match List.nth names !count with
- | Some s -> Cic.Name s
- | None -> Cic.Anonymous
- in
- incr count;
- name
- end else
- FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
-
-type eval_ast =
- {ea_go:
- 'term 'lazy_term 'reduction 'obj 'ident.
-
- disambiguate_command:
- (GrafiteTypes.status ->
- (('term,'obj) GrafiteAst.command) disambiguator_input ->
- GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) ->
-
- disambiguate_macro:
- (GrafiteTypes.status ->
- (('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) ->
-
- ?do_heavy_checks:bool ->
- GrafiteTypes.status ->
- (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement)
- disambiguator_input ->
- GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
- }
-
-type 'a eval_command =
- {ec_go: 'term 'obj.
- disambiguate_command:
- (GrafiteTypes.status -> (('term,'obj) GrafiteAst.command) disambiguator_input ->
- GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) ->
- options -> GrafiteTypes.status ->
- (('term,'obj) GrafiteAst.command) disambiguator_input ->
- GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
- }
-
-type 'a eval_comment =
- {ecm_go: 'term 'lazy_term 'reduction_kind 'obj 'ident.
- disambiguate_command:
- (GrafiteTypes.status -> (('term,'obj) GrafiteAst.command) disambiguator_input ->
- GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) ->
- options -> GrafiteTypes.status ->
- (('term,'lazy_term,'reduction_kind,'obj,'ident) GrafiteAst.comment) disambiguator_input ->
- GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
- }
-
-type 'a eval_executable =
- {ee_go: 'term 'lazy_term 'reduction 'obj 'ident.
-
- disambiguate_command:
- (GrafiteTypes.status ->
- (('term,'obj) GrafiteAst.command) disambiguator_input ->
- GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) ->
-
- disambiguate_macro:
- (GrafiteTypes.status ->
- (('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) ->
-
- options ->
- GrafiteTypes.status ->
- (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code) disambiguator_input ->
- GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
- }
-
-type 'a eval_from_moo =
- { efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status }
-
-let coercion_moo_statement_of (uri,arity, saturations,_) =
- GrafiteAst.Coercion
- (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
-
let basic_eval_unification_hint (t,n) status =
NCicUnifHint.add_user_provided_hint status t n
;;
let inject_unification_hint =
let basic_eval_unification_hint (t,n)
- ~refresh_uri_in_universe
- ~refresh_uri_in_term
+ ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+ ~alias_only status
=
- let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n)
+ if not alias_only then
+ let t = refresh_uri_in_term (status :> NCic.status) t in
+ basic_eval_unification_hint (t,n) status
+ else
+ status
in
- NCicLibrary.Serializer.register#run "unification_hints"
- object(_ : 'a NCicLibrary.register_type)
- method run = basic_eval_unification_hint
- end
+ GrafiteTypes.Serializer.register#run "unification_hints"
+ basic_eval_unification_hint
;;
let eval_unification_hint status t n =
let metasenv,subst,status,t =
- GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,t) in
+ GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,t) in
assert (metasenv=[]);
- let t = NCicUntrusted.apply_subst subst [] t in
+ let t = NCicUntrusted.apply_subst status subst [] t in
let status = basic_eval_unification_hint (t,n) status in
- let dump = inject_unification_hint (t,n)::status#dump in
- let status = status#set_dump dump in
- status,`New []
+ NCicLibrary.dump_obj status (inject_unification_hint (t,n))
;;
let basic_index_obj l status =
status#auto_cache l)
;;
+let basic_eval_interpretation ~alias_only (dsc, (symbol, args), cic_appl_pattern) status =
+ let status =
+ if not alias_only then
+ Interpretations.add_interpretation status dsc (symbol, args) cic_appl_pattern
+ else
+ status
+ in
+ let mode = GrafiteAst.WithPreferences (*assert false*) in (* MATITA 1.0 VEDI SOTTO *)
+ let diff =
+ [DisambiguateTypes.Symbol (symbol, 0), GrafiteAst.Symbol_alias (symbol,0,dsc)]
+ in
+ GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff
+;;
+
+let inject_interpretation =
+ let basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern)
+ ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+ ~alias_only
+ =
+ let rec refresh =
+ function
+ NotationPt.NRefPattern (NReference.Ref (uri,spec)) ->
+ NotationPt.NRefPattern
+ (NReference.reference_of_spec (NCicLibrary.refresh_uri uri) spec)
+ | NotationPt.VarPattern _
+ | NotationPt.ImplicitPattern as x -> x
+ | NotationPt.ApplPattern l -> NotationPt.ApplPattern (List.map refresh l)
+ in
+ let cic_appl_pattern = refresh cic_appl_pattern in
+ basic_eval_interpretation ~alias_only (dsc, (symbol, args), cic_appl_pattern)
+ in
+ GrafiteTypes.Serializer.register#run "interpretation"
+ basic_eval_interpretation
+;;
+
+let eval_interpretation status data=
+ let status = basic_eval_interpretation ~alias_only:false data status in
+ NCicLibrary.dump_obj status (inject_interpretation data)
+;;
+
+let basic_eval_alias (mode,diff) status =
+ GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff
+;;
+
+let inject_alias =
+ let basic_eval_alias (mode,diff) ~refresh_uri_in_universe ~refresh_uri_in_term
+ ~refresh_uri_in_reference ~alias_only =
+ basic_eval_alias (mode,diff)
+ in
+ GrafiteTypes.Serializer.register#run "alias" basic_eval_alias
+;;
+
+let eval_alias status data=
+ let status = basic_eval_alias data status in
+ NCicLibrary.dump_obj status (inject_alias data)
+;;
+
+let basic_eval_input_notation (l1,l2) status =
+ GrafiteParser.extend status l1
+ (fun env loc ->
+ NotationPt.AttributedTerm
+ (`Loc loc,TermContentPres.instantiate_level2 status env l2))
+;;
+
+let inject_input_notation =
+ let basic_eval_input_notation (l1,l2)
+ ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+ ~alias_only status
+ =
+ if not alias_only then
+ let l1 =
+ CicNotationParser.refresh_uri_in_checked_l1_pattern
+ ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))
+ ~refresh_uri_in_reference l1 in
+ let l2 = NotationUtil.refresh_uri_in_term
+ ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))
+ ~refresh_uri_in_reference l2
+ in
+ basic_eval_input_notation (l1,l2) status
+ else
+ status
+ in
+ GrafiteTypes.Serializer.register#run "input_notation"
+ basic_eval_input_notation
+;;
+
+let eval_input_notation status data=
+ let status = basic_eval_input_notation data status in
+ NCicLibrary.dump_obj status (inject_input_notation data)
+;;
+
+let basic_eval_output_notation (l1,l2) status =
+ TermContentPres.add_pretty_printer status l2 l1
+;;
+
+let inject_output_notation =
+ let basic_eval_output_notation (l1,l2)
+ ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+ ~alias_only status
+ =
+ if not alias_only then
+ let l1 =
+ CicNotationParser.refresh_uri_in_checked_l1_pattern
+ ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))
+ ~refresh_uri_in_reference l1 in
+ let l2 = NotationUtil.refresh_uri_in_term
+ ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))
+ ~refresh_uri_in_reference l2
+ in
+ basic_eval_output_notation (l1,l2) status
+ else
+ status
+ in
+ GrafiteTypes.Serializer.register#run "output_notation"
+ basic_eval_output_notation
+;;
+
+let eval_output_notation status data=
+ let status = basic_eval_output_notation data status in
+ NCicLibrary.dump_obj status (inject_output_notation data)
+;;
+
let record_index_obj =
- let aux l
- ~refresh_uri_in_universe
- ~refresh_uri_in_term
+ let aux l ~refresh_uri_in_universe
+ ~refresh_uri_in_term ~refresh_uri_in_reference ~alias_only status
=
+ let refresh_uri_in_term = refresh_uri_in_term (status:>NCic.status) in
+ if not alias_only then
basic_index_obj
(List.map
(fun ks,v -> List.map refresh_uri_in_term ks, refresh_uri_in_term v)
- l)
+ l) status
+ else
+ status
in
- NCicLibrary.Serializer.register#run "index_obj"
- object(_ : 'a NCicLibrary.register_type)
- method run = aux
- end
+ GrafiteTypes.Serializer.register#run "index_obj" aux
;;
let compute_keys status uri height kind =
if keys <> [] then
begin
HLog.debug ("Indexing:" ^
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
+ status#ppterm ~metasenv:[] ~subst:[] ~context:[] t);
HLog.debug ("With keys:" ^ String.concat "\n" (List.map (fun t ->
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t) keys));
+ status#ppterm ~metasenv:[] ~subst:[] ~context:[] t) keys));
Some (keys,t)
end
else
begin
HLog.debug ("Not indexing:" ^
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
+ status#ppterm ~metasenv:[] ~subst:[] ~context:[] t);
None
end)
data
(*prerr_endline (string_of_int height);*)
let data = compute_keys status uri height kind in
let status = basic_index_obj data status in
- let dump = record_index_obj data :: status#dump in
- status#set_dump dump
+ NCicLibrary.dump_obj status (record_index_obj data)
;;
let index_eq uri status =
let eq_status = status#eq_cache in
- let eq_status1 = NCicParamod.index_obj eq_status uri in
- status#set_eq_cache eq_status1
+ let eq_status = NCicParamod.index_obj status eq_status uri in
+ status#set_eq_cache eq_status
;;
let record_index_eq =
let basic_index_eq uri
- ~refresh_uri_in_universe
- ~refresh_uri_in_term
- = index_eq (NCicLibrary.refresh_uri uri)
+ ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+ ~alias_only status
+ = if not alias_only then index_eq (NCicLibrary.refresh_uri uri) status else
+ status
in
- NCicLibrary.Serializer.register#run "index_eq"
- object(_ : 'a NCicLibrary.register_type)
- method run = basic_index_eq
- end
+ GrafiteTypes.Serializer.register#run "index_eq" basic_index_eq
;;
let index_eq_for_auto status uri =
if newstatus#eq_cache == status#eq_cache then status
else
((*prerr_endline ("recording " ^ (NUri.string_of_uri uri));*)
- let dump = record_index_eq uri :: newstatus#dump
- in newstatus#set_dump dump)
+ NCicLibrary.dump_obj newstatus (record_index_eq uri))
else
((*prerr_endline "Not a fact";*)
status)
;;
-let basic_eval_add_constraint (u1,u2) status =
- NCicLibrary.add_constraint status u1 u2
-;;
-
let inject_constraint =
let basic_eval_add_constraint (u1,u2)
- ~refresh_uri_in_universe
- ~refresh_uri_in_term
+ ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+ ~alias_only status
=
- let u1 = refresh_uri_in_universe u1 in
- let u2 = refresh_uri_in_universe u2 in
- basic_eval_add_constraint (u1,u2)
+ if not alias_only then
+ let u1 = refresh_uri_in_universe u1 in
+ let u2 = refresh_uri_in_universe u2 in
+ (* NCicLibrary.add_constraint adds the constraint to the NCicEnvironment
+ * and also to the storage (for undo/redo). During inclusion of compiled
+ * files the storage must not be touched. *)
+ NCicEnvironment.add_lt_constraint u1 u2;
+ status
+ else
+ status
in
- NCicLibrary.Serializer.register#run "constraints"
- object(_:'a NCicLibrary.register_type)
- method run = basic_eval_add_constraint
- end
+ GrafiteTypes.Serializer.register#run "constraints" basic_eval_add_constraint
;;
let eval_add_constraint status u1 u2 =
- let status = basic_eval_add_constraint (u1,u2) status in
- let dump = inject_constraint (u1,u2)::status#dump in
- let status = status#set_dump dump in
- status,`Old []
-;;
-
-let add_coercions_of_lemmas lemmas status =
- let moo_content =
- HExtlib.filter_map
- (fun uri ->
- match CoercDb.is_a_coercion (Cic.Const (uri,[])) with
- | None -> None
- | Some (_,tgt,_,sat,_) ->
- let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
- Some (coercion_moo_statement_of (uri,arity,sat,0)))
- lemmas
- in
- let status = GrafiteTypes.add_moo_content moo_content status in
- status#set_coercions (CoercDb.dump ()),
- lemmas
-
-let eval_coercion status ~add_composites uri arity saturations =
- let uri =
- try CicUtil.uri_of_term uri
- with Invalid_argument _ ->
- raise (Invalid_argument "coercion can only be constants/constructors")
- in
- let status, lemmas =
- GrafiteSync.add_coercion ~add_composites
- ~pack_coercion_obj:CicRefine.pack_coercion_obj
- status uri arity saturations status#baseuri in
- let moo_content = coercion_moo_statement_of (uri,arity,saturations,0) in
- let status = GrafiteTypes.add_moo_content [moo_content] status in
- add_coercions_of_lemmas lemmas status
-
-let eval_prefer_coercion status c =
- let uri =
- try CicUtil.uri_of_term c
- with Invalid_argument _ ->
- raise (Invalid_argument "coercion can only be constants/constructors")
- in
- let status = GrafiteSync.prefer_coercion status uri in
- let moo_content = GrafiteAst.PreferCoercion (HExtlib.dummy_floc,c) in
- let status = GrafiteTypes.add_moo_content [moo_content] status in
- status, `Old []
-
-let eval_ng_punct (_text, _prefix_len, punct) =
- match punct with
- | GrafiteAst.Dot _ -> NTactics.dot_tac
- | GrafiteAst.Semicolon _ -> fun x -> x
- | GrafiteAst.Branch _ -> NTactics.branch_tac ~force:false
- | GrafiteAst.Shift _ -> NTactics.shift_tac
- | GrafiteAst.Pos (_,l) -> NTactics.pos_tac l
- | GrafiteAst.Wildcard _ -> NTactics.wildcard_tac
- | GrafiteAst.Merge _ -> NTactics.merge_tac
+ let status = NCicLibrary.add_constraint status u1 u2 in
+ NCicLibrary.dump_obj status (inject_constraint (u1,u2))
;;
let eval_ng_tac tac =
| GrafiteAst.NCut (_loc, t) -> NTactics.cut_tac (text,prefix_len,t)
(*| GrafiteAst.NDiscriminate (_,what) -> NDestructTac.discriminate_tac ~what:(text,prefix_len,what)
| GrafiteAst.NSubst (_,what) -> NDestructTac.subst_tac ~what:(text,prefix_len,what)*)
+ | GrafiteAst.NClear (_loc, l) -> NTactics.clear_tac l
| GrafiteAst.NDestruct (_,dom,skip) -> NDestructTac.destruct_tac dom skip
| GrafiteAst.NDot _ -> NTactics.dot_tac
| GrafiteAst.NElim (_loc, what, where) ->
| GrafiteAst.NUnfocus _ -> NTactics.unfocus_tac
| GrafiteAst.NWildcard _ -> NTactics.wildcard_tac
| GrafiteAst.NTry (_,tac) -> NTactics.try_tac
- (aux f (text, prefix_len, tac))
+ (f f (text, prefix_len, tac))
| GrafiteAst.NAssumption _ -> NTactics.assumption_tac
| GrafiteAst.NBlock (_,l) ->
NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l)
let u,h,metasenv, subst,o = status#obj in
let o =
NCicUntrusted.map_obj_kind ~skip_body:true
- (NCicUntrusted.apply_subst subst []) o
+ (NCicUntrusted.apply_subst status subst []) o
in
- status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o)
+ status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv status subst metasenv,subst,o)
+;;
+
+let is_proof_irrelevant status context ty =
+ match
+ NCicReduction.whd status ~subst:[] context
+ (NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] context ty)
+ with
+ NCic.Sort NCic.Prop -> true
+ | NCic.Sort _ -> false
+ | _ -> assert false
+;;
+
+let rec relevance_of status ?(context=[]) ty =
+ match NCicReduction.whd status ~subst:[] context ty with
+ NCic.Prod (n,s,t) ->
+ not (is_proof_irrelevant status context s) ::
+ relevance_of status ~context:((n,NCic.Decl s)::context) t
+ | _ -> []
+;;
+
+let compute_relevance status uri =
+ function
+ NCic.Constant (_,name,bo,ty,attrs) ->
+ let relevance = relevance_of status ty in
+ NCic.Constant (relevance,name,bo,ty,attrs)
+ | NCic.Fixpoint (ind,funs,attrs) ->
+ let funs =
+ List.map
+ (fun (_,name,recno,ty,bo) ->
+ let relevance = relevance_of status ty in
+ relevance,name,recno,ty,bo
+ ) funs
+ in
+ NCic.Fixpoint (ind,funs,attrs)
+ | NCic.Inductive (ind,leftno,tys,attrs) ->
+ let context =
+ List.rev_map (fun (_,name,arity,_) -> name,NCic.Decl arity) tys in
+ let tysno = List.length tys in
+ let tys =
+ List.map
+ (fun (_,name,arity,cons) ->
+ let relevance = relevance_of status arity in
+ let cons =
+ List.map
+ (fun (_,name,ty) ->
+ let dety =
+ NCicTypeChecker.debruijn status uri tysno ~subst:[] [] ty in
+ let relevance = relevance_of status ~context dety in
+ relevance,name,ty
+ ) cons
+ in
+ (relevance,name,arity,cons)
+ ) tys
+ in
+ NCic.Inductive (ind,leftno,tys,attrs)
;;
-let rec eval_ncommand opts status (text,prefix_len,cmd) =
+let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
match cmd with
+ | GrafiteAst.Include (loc, mode, fname) ->
+ let _root, baseuri, fullpath, _rrelpath =
+ Librarian.baseuri_of_script ~include_paths fname in
+ let baseuri = NUri.uri_of_string baseuri in
+ (* MATITA 1.0: keep WithoutPreferences? *)
+ let alias_only = (mode = GrafiteAst.OnlyPreferences) in
+ GrafiteTypes.Serializer.require
+ ~alias_only ~baseuri ~fname:fullpath status
| GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
| GrafiteAst.NCoercion (loc, name, t, ty, source, target) ->
- NCicCoercDeclaration.eval_ncoercion status name t ty source target
+ let status, composites =
+ NCicCoercDeclaration.eval_ncoercion status name t ty source target in
+ let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
+ let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
+ eval_alias status (mode,aliases)
| GrafiteAst.NQed loc ->
if status#ng_mode <> `ProofMode then
raise (GrafiteTypes.Command_error "Not in proof mode")
else
let obj_kind =
NCicUntrusted.map_obj_kind
- (NCicUntrusted.apply_subst subst []) obj_kind in
- let height = NCicTypeChecker.height_of_obj_kind uri [] obj_kind in
+ (NCicUntrusted.apply_subst status subst []) obj_kind in
+ let height = NCicTypeChecker.height_of_obj_kind status uri [] obj_kind in
(* fix the height inside the object *)
let rec fix () = function
| NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri ->
| NReference.CoFix _ -> NReference.CoFix height
| NReference.Ind _ | NReference.Con _
| NReference.Decl as s -> s))
- | t -> NCicUtils.map (fun _ () -> ()) () fix t
+ | t -> NCicUtils.map status (fun _ () -> ()) () fix t
in
let obj_kind =
match obj_kind with
NCicUntrusted.map_obj_kind (fix ()) obj_kind
| _ -> obj_kind
in
+ let obj_kind = compute_relevance status uri obj_kind in
let obj = uri,height,[],[],obj_kind in
- prerr_endline ("pp new obj \n"^NCicPp.ppobj obj);
let old_status = status in
let status = NCicLibrary.add_obj status obj in
let index_obj =
index_eq uri status
with _ -> prerr_endline "got an exception"; status
in *)
-(* prerr_endline (NCicPp.ppobj obj); *)
+(* prerr_endline (status#ppobj obj); *)
HLog.message ("New object: " ^ NUri.string_of_uri uri);
(try
- (*prerr_endline (NCicPp.ppobj obj);*)
- let boxml = NCicElim.mk_elims obj in
- let boxml = boxml @ NCicElim.mk_projections obj in
-(*
- let objs = [] in
- let timestamp,uris_rev =
- List.fold_left
- (fun (status,uris_rev) (uri,_,_,_,_) as obj ->
- let status = NCicLibrary.add_obj status obj in
- status,uri::uris_rev
- ) (status,[]) objs in
- let uris = uri::List.rev uris_rev in
-*)
+ (*prerr_endline (status#ppobj obj);*)
+ let boxml = NCicElim.mk_elims status obj in
+ let boxml = boxml @ NCicElim.mk_projections status obj in
let status = status#set_ng_mode `CommandMode in
- let status = LexiconSync.add_aliases_for_objs status (`New [uri]) in
- let status,uris =
+ let xxaliases = GrafiteDisambiguate.aliases_for_objs status [uri] in
+ let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
+ let status = eval_alias status (mode,xxaliases) in
+ let status =
List.fold_left
- (fun (status,uris) boxml ->
+ (fun status boxml ->
try
- let nstatus,nuris =
- eval_ncommand opts status
+ let nstatus =
+ eval_ncommand ~include_paths opts status
("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
in
if nstatus#ng_mode <> `CommandMode then
begin
(*HLog.warn "error in generating projection/eliminator";*)
- status, uris
+ assert(status#ng_mode = `CommandMode);
+ status
end
else
- nstatus, concat_nuris uris nuris
+ nstatus
with
| MultiPassDisambiguator.DisambiguationError _
| NCicTypeChecker.TypeCheckerFailure _ ->
(*HLog.warn "error in generating projection/eliminator";*)
- status,uris
- ) (status,`New [] (* uris *)) boxml in
+ status
+ ) status boxml in
let _,_,_,_,nobj = obj in
let status = match nobj with
NCic.Inductive (is_ind,leftno,[it],_) ->
(snd (NCicElim.ast_of_sort outsort)))
is_ind it leftno outsort status status#baseuri in
let _,_,menv,_,_ = invobj in
- fst (match menv with
- [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
- | _ -> status,`New []))
+ (match menv with
+ [] -> eval_ncommand ~include_paths opts status
+ ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+ | _ -> status))
(* XXX *)
with _ -> (*HLog.warn "error in generating inversion principle"; *)
let status = status#set_ng_mode `CommandMode in status)
(fun (name,is_coercion,arity) ->
if is_coercion then Some(name,leftno,arity) else None) fields
| _ -> [] in
- let status,uris =
+ let status =
List.fold_left
- (fun (status,uris) (name,cpos,arity) ->
+ (fun status (name,cpos,arity) ->
try
let metasenv,subst,status,t =
- GrafiteDisambiguate.disambiguate_nterm None status [] [] []
- ("",0,CicNotationPt.Ident (name,None)) in
+ GrafiteDisambiguate.disambiguate_nterm status None [] [] []
+ ("",0,NotationPt.Ident (name,None)) in
assert (metasenv = [] && subst = []);
let status, nuris =
NCicCoercDeclaration.
basic_eval_and_record_ncoercion_from_t_cpos_arity
- status (name,t,cpos,arity)
- in
- let uris = concat_nuris nuris uris in
- status, uris
+ status (name,t,cpos,arity) in
+ let aliases = GrafiteDisambiguate.aliases_for_objs status nuris in
+ eval_alias status (mode,aliases)
with MultiPassDisambiguator.DisambiguationError _->
HLog.warn ("error in generating coercion: "^name);
- status, uris)
- (status,uris) coercions
+ status)
+ status coercions
in
- status,uris
+ status
with
exn ->
NCicLibrary.time_travel old_status;
raise (GrafiteTypes.Command_error "Not in command mode")
else
let tgt_uri_ext, old_ok =
- match NCicEnvironment.get_checked_obj src_uri with
+ match NCicEnvironment.get_checked_obj status src_uri with
| _,_,[],[], (NCic.Inductive _ as ok) -> ".ind", ok
| _,_,[],[], (NCic.Fixpoint _ as ok) -> ".con", ok
| _,_,[],[], (NCic.Constant _ as ok) -> ".con", ok
(try NCic.Const
(NReference.reference_of_spec (List.assoc u map)spec)
with Not_found -> t)
- | t -> NCicUtils.map (fun _ _ -> ()) () subst t
+ | t -> NCicUtils.map status (fun _ _ -> ()) () subst t
in
NCicUntrusted.map_obj_kind ~skip_body:false (subst ()) old_ok
in
let ninitial_stack = Continuationals.Stack.of_nmetasenv [] in
let status = status#set_obj (tgt_uri,0,[],[],ok) in
- (*prerr_endline (NCicPp.ppobj (tgt_uri,0,[],[],ok));*)
+ (*prerr_endline (status#ppobj (tgt_uri,0,[],[],ok));*)
let status = status#set_stack ninitial_stack in
let status = subst_metasenv_and_fix_names status in
let status = status#set_ng_mode `ProofMode in
- eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+ eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
| GrafiteAst.NObj (loc,obj) ->
if status#ng_mode <> `CommandMode then
raise (GrafiteTypes.Command_error "Not in command mode")
let status = status#set_ng_mode `ProofMode in
(match nmenv with
[] ->
- eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
- | _ -> status,`New [])
+ eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+ | _ -> status)
| GrafiteAst.NDiscriminator (_,_) -> assert false (*(loc, indty) ->
if status#ng_mode <> `CommandMode then
raise (GrafiteTypes.Command_error "Not in command mode")
let status,obj = NDestructTac.mk_discriminator it status in
let _,_,menv,_,_ = obj in
(match menv with
- [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+ [] -> eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
| _ -> prerr_endline ("Discriminator: non empty metasenv");
- status, `New []) *)
+ status, []) *)
| GrafiteAst.NInverter (loc, name, indty, selection, sort) ->
if status#ng_mode <> `CommandMode then
raise (GrafiteTypes.Command_error "Not in command mode")
else
let metasenv,subst,status,sort = match sort with
| None -> [],[],status,NCic.Sort NCic.Prop
- | Some s -> GrafiteDisambiguate.disambiguate_nterm None status [] [] []
- (text,prefix_len,s)
+ | Some s ->
+ GrafiteDisambiguate.disambiguate_nterm status None [] [] []
+ (text,prefix_len,s)
in
assert (metasenv = []);
- let sort = NCicReduction.whd ~subst [] sort in
- let sort = match sort with
+ let sort = NCicReduction.whd status ~subst [] sort in
+ let sort =
+ match sort with
NCic.Sort s -> s
- | _ -> raise (Invalid_argument (Printf.sprintf "ninverter: found target %s, which is not a sort"
- (NCicPp.ppterm ~metasenv ~subst ~context:[] sort)))
- in
+ | _ ->
+ raise (Invalid_argument (Printf.sprintf
+ "ninverter: found target %s, which is not a sort"
+ (status#ppterm ~metasenv ~subst ~context:[] sort))) in
let status = status#set_ng_mode `ProofMode in
let metasenv,subst,status,indty =
- GrafiteDisambiguate.disambiguate_nterm None status [] [] subst (text,prefix_len,indty) in
- let indtyno,(_,leftno,tys,_,_) = match indty with
- NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,_))) as r) ->
- indtyno, NCicEnvironment.get_checked_indtys r
- | _ -> prerr_endline ("engine: indty =" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] indty) ; assert false in
+ GrafiteDisambiguate.disambiguate_nterm status None [] [] subst
+ (text,prefix_len,indty) in
+ let indtyno,(_,leftno,tys,_,_) =
+ match indty with
+ NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,_))) as r) ->
+ indtyno, NCicEnvironment.get_checked_indtys status r
+ | _ ->
+ prerr_endline ("engine: indty =" ^ status#ppterm ~metasenv:[]
+ ~subst:[] ~context:[] indty);
+ assert false in
let it = List.nth tys indtyno in
- let status,obj = NInversion.mk_inverter name true it leftno ?selection sort
- status status#baseuri in
- let _,_,menv,_,_ = obj in
- (match menv with
- [] ->
- eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
- | _ -> assert false)
+ let status,obj =
+ NInversion.mk_inverter name true it leftno ?selection sort
+ status status#baseuri in
+ let _,_,menv,_,_ = obj in
+ (match menv with
+ [] ->
+ eval_ncommand ~include_paths opts status
+ ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+ | _ -> assert false)
| GrafiteAst.NUnivConstraint (loc,u1,u2) ->
eval_add_constraint status [`Type,u1] [`Type,u2]
-;;
-
-let rec eval_command = {ec_go = fun ~disambiguate_command opts status
-(text,prefix_len,cmd) ->
- let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
- let status,uris =
- match cmd with
- | GrafiteAst.PreferCoercion (loc, coercion) ->
- eval_prefer_coercion status coercion
- | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) ->
- let res,uris =
- eval_coercion status ~add_composites uri arity saturations
+ (* ex lexicon commands *)
+ | GrafiteAst.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) ->
+ let cic_appl_pattern =
+ GrafiteDisambiguate.disambiguate_cic_appl_pattern status args
+ cic_appl_pattern
in
- res,`Old uris
- | GrafiteAst.Default (loc, what, uris) as cmd ->
- LibraryObjects.set_default what uris;
- GrafiteTypes.add_moo_content [cmd] status,`Old []
- | GrafiteAst.Drop loc -> raise Drop
- | GrafiteAst.Include (loc, mode, new_or_old, baseuri) ->
- (* Old Include command is not recursive; new one is *)
- let status =
- if new_or_old = `OldAndNew then
- let moopath_rw, moopath_r =
- LibraryMisc.obj_file_of_baseuri
- ~must_exist:false ~baseuri ~writable:true,
- LibraryMisc.obj_file_of_baseuri
- ~must_exist:false ~baseuri ~writable:false in
- let moopath =
- if Sys.file_exists moopath_r then moopath_r else
- if Sys.file_exists moopath_rw then moopath_rw else
- raise (IncludedFileNotCompiled (moopath_rw,baseuri))
- in
- eval_from_moo.efm_go status moopath
- else
- status
- in
- let status =
- NCicLibrary.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
- status in
+ eval_interpretation status (dsc,(symbol, args),cic_appl_pattern)
+ | GrafiteAst.Notation (loc, dir, l1, associativity, precedence, l2) ->
+ let l1 =
+ CicNotationParser.check_l1_pattern
+ l1 (dir = Some `RightToLeft) precedence associativity
+ in
let status =
- GrafiteTypes.add_moo_content
- [GrafiteAst.Include (loc,mode,`New,baseuri)] status
+ if dir <> Some `RightToLeft then eval_input_notation status (l1,l2)
+ else status
in
- status,`Old []
- | GrafiteAst.Print (_,_) -> status,`Old []
- | GrafiteAst.Set (loc, name, value) -> status, `Old []
-(* GrafiteTypes.set_option status name value,[] *)
- | GrafiteAst.Obj (loc,obj) -> (* MATITA 1.0 *) assert false
- in
- status,uris
+ if dir <> Some `LeftToRight then eval_output_notation status (l1,l2)
+ else status
+ | GrafiteAst.Alias (loc, spec) ->
+ let diff =
+ (*CSC: Warning: this code should be factorized with the corresponding
+ code in DisambiguatePp *)
+ match spec with
+ | GrafiteAst.Ident_alias (id,uri) ->
+ [DisambiguateTypes.Id id,spec]
+ | GrafiteAst.Symbol_alias (symb, instance, desc) ->
+ [DisambiguateTypes.Symbol (symb,instance),spec]
+ | GrafiteAst.Number_alias (instance,desc) ->
+ [DisambiguateTypes.Num instance,spec]
+ in
+ let mode = GrafiteAst.WithPreferences in(*assert false in (* VEDI SOPRA *) MATITA 1.0*)
+ eval_alias status (mode,diff)
+;;
+
+let eval_comment opts status (text,prefix_len,c) = status
-} and eval_executable = {ee_go = fun ~disambiguate_command
-~disambiguate_macro opts status (text,prefix_len,ex) ->
+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
subst_metasenv_and_fix_names status)
status tacl
in
- status,`New []
- | GrafiteAst.Command (_, cmd) ->
- eval_command.ec_go ~disambiguate_command opts status (text,prefix_len,cmd)
+ status
| GrafiteAst.NCommand (_, cmd) ->
- eval_ncommand opts status (text,prefix_len,cmd)
- | GrafiteAst.Macro (loc, macro) ->
- raise (Macro (loc,disambiguate_macro status (text,prefix_len,macro)))
+ eval_ncommand ~include_paths opts status (text,prefix_len,cmd)
| GrafiteAst.NMacro (loc, macro) ->
raise (NMacro (loc,macro))
-} and eval_from_moo = {efm_go = fun status fname ->
- let ast_of_cmd cmd =
- ("",0,GrafiteAst.Executable (HExtlib.dummy_floc,
- GrafiteAst.Command (HExtlib.dummy_floc,
- cmd)))
- in
- let moo = GrafiteMarshal.load_moo fname in
- List.fold_left
- (fun status ast ->
- let ast = ast_of_cmd ast in
- let status,lemmas =
- eval_ast.ea_go
- ~disambiguate_command:(fun status (_,_,cmd) -> status,cmd)
- ~disambiguate_macro:(fun _ _ -> assert false)
- status ast
- in
- assert (lemmas=`Old []);
- status)
- status moo
-} and eval_ast = {ea_go = fun ~disambiguate_command
-~disambiguate_macro ?(do_heavy_checks=false) status
-(text,prefix_len,st)
-->
+and eval_ast ~include_paths ?(do_heavy_checks=false) status (text,prefix_len,st)
+=
let opts = { do_heavy_checks = do_heavy_checks ; } in
match st with
| GrafiteAst.Executable (_,ex) ->
- eval_executable.ee_go ~disambiguate_command
- ~disambiguate_macro opts status (text,prefix_len,ex)
+ eval_executable ~include_paths opts status (text,prefix_len,ex)
| GrafiteAst.Comment (_,c) ->
- eval_comment.ecm_go ~disambiguate_command opts status (text,prefix_len,c)
-} and eval_comment = { ecm_go = fun ~disambiguate_command opts status (text,prefix_len,c) ->
- status, `Old []
-}
+ eval_comment opts status (text,prefix_len,c)
;;
-
-
-let eval_ast = eval_ast.ea_go