X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=b471bece3e44ad26548f5e432ddb793232319490;hb=70aa6dc959dc1d49f751c183367c3b73393c938b;hp=8eb438e185866d44507e65fbc12496650ff80d9c;hpb=53a5acbe28212706be9c684d612aee1ccb165587;p=helm.git diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 8eb438e18..b471bece3 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -25,7 +25,6 @@ (* $Id$ *) -exception Drop (* mo file name, ma file name *) exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro @@ -58,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 = @@ -198,7 +197,7 @@ 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 = @@ -292,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") @@ -367,28 +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";*) assert(status#ng_mode = `CommandMode); - status, uris + 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],_) -> @@ -403,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) @@ -423,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 [] [] [] @@ -436,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; @@ -478,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") @@ -494,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") @@ -511,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) -> @@ -543,29 +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] + (* 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 = + 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 + 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 = + if dir <> Some `RightToLeft then + GrafiteParser.extend status l1 + (fun env loc -> + NotationPt.AttributedTerm + (`Loc loc,TermContentPres.instantiate_level2 env l2)) + else status + in + 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 *) ;; -let eval_comment opts status (text,prefix_len,c) = status, [] - -let rec eval_command opts status (text,prefix_len,cmd) = - let status,uris = - match cmd with - | GrafiteAst.Include (loc, baseuri) -> - let status,obj = - GrafiteTypes.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) - status in - let status = status#set_dump (obj::status#dump) in - status,[] - | GrafiteAst.Print (_,_) -> status,[] - | GrafiteAst.Set (loc, name, value) -> status, [] - in - status,uris +let eval_comment opts status (text,prefix_len,c) = status -and eval_executable 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 @@ -578,19 +655,18 @@ and eval_executable opts status (text,prefix_len,ex) = subst_metasenv_and_fix_names status) status tacl in - status,[] - | GrafiteAst.Command (_, cmd) -> - eval_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_ast ?(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 opts status (text,prefix_len,ex) + eval_executable ~include_paths opts status (text,prefix_len,ex) | GrafiteAst.Comment (_,c) -> eval_comment opts status (text,prefix_len,c) ;;