X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=b471bece3e44ad26548f5e432ddb793232319490;hb=70aa6dc959dc1d49f751c183367c3b73393c938b;hp=1a87934a595cb4c1406d49b39ba81a844f4909f6;hpb=47a9eb47d4215450230840bc66570ce412d0ce79;p=helm.git diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 1a87934a5..b471bece3 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -25,9 +25,7 @@ (* $Id$ *) -exception Drop (* mo file name, ma file name *) -(*exception IncludedFileNotCompiled of string * string *) exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro type 'a disambiguator_input = string * int * 'a @@ -47,10 +45,8 @@ let inject_unification_hint = = let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n) 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 = @@ -61,7 +57,7 @@ let eval_unification_hint status t n = 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,[] + status ;; let basic_index_obj l status = @@ -84,10 +80,7 @@ let record_index_obj = (fun ks,v -> List.map refresh_uri_in_term ks, refresh_uri_in_term v) l) 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 = @@ -168,10 +161,7 @@ let record_index_eq = ~refresh_uri_in_term = index_eq (NCicLibrary.refresh_uri uri) 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 = @@ -200,17 +190,14 @@ let inject_constraint = let u2 = refresh_uri_in_universe u2 in basic_eval_add_constraint (u1,u2) 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,[] + status ;; let eval_ng_tac tac = @@ -304,11 +291,24 @@ let subst_metasenv_and_fix_names status = ;; -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 status,obj = + GrafiteTypes.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) + status in + let status = status#set_dump (obj::status#dump) in + assert false; (* mode must be passed to GrafiteTypes.Serializer.require + somehow *) + status | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n | GrafiteAst.NCoercion (loc, name, t, ty, source, target) -> + let status, composites = NCicCoercDeclaration.eval_ncoercion status name t ty source target + in + LexiconSync.add_aliases_for_objs status composites | GrafiteAst.NQed loc -> if status#ng_mode <> `ProofMode then raise (GrafiteTypes.Command_error "Not in proof mode") @@ -341,7 +341,6 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = | _ -> 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 = @@ -380,27 +379,28 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = *) let status = status#set_ng_mode `CommandMode in let status = LexiconSync.add_aliases_for_objs status [uri] in - let status,uris = + 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, uris@nuris + nstatus with | MultiPassDisambiguator.DisambiguationError _ | NCicTypeChecker.TypeCheckerFailure _ -> (*HLog.warn "error in generating projection/eliminator";*) - status,uris - ) (status,[] (* uris *)) boxml in + status + ) status boxml in let _,_,_,_,nobj = obj in let status = match nobj with NCic.Inductive (is_ind,leftno,[it],_) -> @@ -415,9 +415,10 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = (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,[])) + (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) @@ -435,9 +436,9 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = (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 [] [] [] @@ -448,14 +449,13 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = basic_eval_and_record_ncoercion_from_t_cpos_arity status (name,t,cpos,arity) in - let uris = nuris@uris in - status, uris + LexiconSync.add_aliases_for_objs status nuris 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; @@ -490,7 +490,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = 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") @@ -506,8 +506,8 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = let status = status#set_ng_mode `ProofMode in (match nmenv with [] -> - eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) - | _ -> status,[]) + 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") @@ -523,7 +523,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = 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, []) *) | GrafiteAst.NInverter (loc, name, indty, selection, sort) -> @@ -555,48 +555,94 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = 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) | _ -> assert false) | GrafiteAst.NUnivConstraint (loc,u1,u2) -> eval_add_constraint status [`Type,u1] [`Type,u2] -;; - -let eval_comment ~disambiguate_command opts status (text,prefix_len,c) = - status, [] - -let rec eval_command ~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.Include (loc, baseuri) -> - (* + (* ex lexicon commands *) + | GrafiteAst.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) -> + let rec disambiguate = + function + NotationPt.ApplPattern l -> + NotationPt.ApplPattern (List.map disambiguate l) + | NotationPt.VarPattern id + when not + (List.exists + (function (NotationPt.IdentArg (_,id')) -> id'=id) args) + -> + let item = DisambiguateTypes.Id id in + begin try + match DisambiguateTypes.Environment.find item status#lstatus.LexiconTypes.aliases with + GrafiteAst.Ident_alias (_, uri) -> + NotationPt.NRefPattern (NReference.reference_of_string uri) + | _ -> assert false + with Not_found -> + prerr_endline + ("LexiconEngine.eval_command: domain item not found: " ^ + (DisambiguateTypes.string_of_domain_item item)); + LexiconEngine.dump_aliases prerr_endline "" status; + raise + (Failure + ((DisambiguateTypes.string_of_domain_item item) ^ " not found")) + end + | p -> p + in + let cic_appl_pattern = disambiguate cic_appl_pattern in let status = - 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 status moopath + Interpretations.add_interpretation status + dsc (symbol, args) cic_appl_pattern in + let mode = GrafiteAst.WithPreferences (*assert false*) in (* VEDI SOTTO *) + let diff = + [DisambiguateTypes.Symbol (symbol, 0), + GrafiteAst.Symbol_alias (symbol,0,dsc)] in + let status = + LexiconEngine.set_proof_aliases status ~implicit_aliases:false mode diff in - let status = *) - NCicLibrary.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) - status (*in + status + (*assert false*) (* MANCA SALVATAGGIO SU DISCO CHE DEVE TENERE IN CONTO + IL MODE WithPreference/WithOutPreferences*) + | 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,baseuri)] status + if dir <> Some `RightToLeft then + GrafiteParser.extend status l1 + (fun env loc -> + NotationPt.AttributedTerm + (`Loc loc,TermContentPres.instantiate_level2 env l2)) + else status in - status,[] *), [] - | GrafiteAst.Print (_,_) -> status,[] - | GrafiteAst.Set (loc, name, value) -> status, [] - in - status,uris + let status = + if dir <> Some `LeftToRight then + let status = TermContentPres.add_pretty_printer status l2 l1 in + status + else + status + in +(* assert false (* MANCA SALVATAGGIO SU DISCO *) *) + status (* capire [] XX *) + | 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 = assert false in (* VEDI SOPRA *) + LexiconEngine.set_proof_aliases status ~implicit_aliases:false mode diff; + assert false (* MANCA SALVATAGGIO SU DISCO *) +;; -and eval_executable ~disambiguate_command opts status (text,prefix_len,ex) = +let eval_comment opts status (text,prefix_len,c) = status + +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 @@ -609,39 +655,18 @@ and eval_executable ~disambiguate_command opts status (text,prefix_len,ex) = subst_metasenv_and_fix_names status) status tacl in - status,[] - | GrafiteAst.Command (_, cmd) -> - eval_command ~disambiguate_command opts status (text,prefix_len,cmd) + status | GrafiteAst.NCommand (_, cmd) -> - eval_ncommand opts status (text,prefix_len,cmd) + eval_ncommand ~include_paths opts status (text,prefix_len,cmd) | GrafiteAst.NMacro (loc, macro) -> raise (NMacro (loc,macro)) -and eval_from_moo 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 ~disambiguate_command:(fun status (_,_,cmd) -> status,cmd) - status ast - in - assert (lemmas=[]); - status) - status moo - -and eval_ast ~disambiguate_command ?(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 ~disambiguate_command opts status (text,prefix_len,ex) + eval_executable ~include_paths opts status (text,prefix_len,ex) | GrafiteAst.Comment (_,c) -> - eval_comment ~disambiguate_command opts status (text,prefix_len,c) + eval_comment opts status (text,prefix_len,c) ;;