From 928af763320668168206e88d93e8a77698f3b925 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Wed, 14 Dec 2011 13:51:15 +0000 Subject: [PATCH] Matitaweb: large commit porting to the new Matita 0.95 syntax. Integrates some old patches. Fixes a bug with GotoPos which prevented errors from being shown. --- .../content_pres/cicNotationParser.ml | 7 +- .../content_pres/cicNotationParser.mli | 3 + matitaB/components/grafite/grafiteAst.ml | 53 +- matitaB/components/grafite/grafiteAstPp.ml | 13 +- .../grafite_engine/grafiteEngine.ml | 54 +- .../grafite_engine/nCicCoercDeclaration.ml | 25 +- .../grafite_engine/nCicCoercDeclaration.mli | 3 +- .../grafite_parser/grafiteParser.ml | 92 ++-- matitaB/components/ng_kernel/nCic.ml | 1 + matitaB/components/ng_kernel/nCicPp.ml | 1 + matitaB/components/ng_tactics/nDestructTac.ml | 494 +++++++++++------- .../components/ng_tactics/nDestructTac.mli | 6 + matitaB/components/ng_tactics/nTactics.mli | 1 + matitaB/matita/matitaweb.js | 211 ++++---- 14 files changed, 552 insertions(+), 412 deletions(-) diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml index 4894218e8..7522d3c79 100644 --- a/matitaB/components/content_pres/cicNotationParser.ml +++ b/matitaB/components/content_pres/cicNotationParser.ml @@ -45,6 +45,7 @@ type ('a,'b,'c,'d,'e) grammars = { sym_attributes: (string option * string option) Grammar.Entry.e; sym_table: (string * Stdpp.location Grammar.Entry.e) list; let_defs: 'c Grammar.Entry.e; + let_codefs: 'c Grammar.Entry.e; protected_binder_vars: 'd Grammar.Entry.e; level2_meta: 'b Grammar.Entry.e; } @@ -672,10 +673,11 @@ END let term = grammars.term in let atag_attributes = grammars.sym_attributes in let let_defs = grammars.let_defs in + let let_codefs = grammars.let_codefs in let ident = grammars.ident in let protected_binder_vars = grammars.protected_binder_vars in EXTEND - GLOBAL: level2_ast term let_defs protected_binder_vars ident atag_attributes; + GLOBAL: level2_ast term let_defs let_codefs protected_binder_vars ident atag_attributes; level2_ast: [ [ p = term -> p ] ]; sort: [ [ "Prop" -> `Prop @@ -938,6 +940,7 @@ let initial_grammars loctable keywords = [] initial_symbols in let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs" in + let let_codefs = Grammar.Entry.create level2_ast_grammar "let_codefs" in let protected_binder_vars = Grammar.Entry.create level2_ast_grammar "protected_binder_vars" in let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta" in @@ -949,6 +952,7 @@ let initial_grammars loctable keywords = sym_table=sym_table; sym_attributes=sym_attributes; let_defs=let_defs; + let_codefs=let_codefs; protected_binder_vars=protected_binder_vars; level2_meta=level2_meta; level2_ast_grammar=level2_ast_grammar; @@ -1025,6 +1029,7 @@ let level2_ast_grammar status = status#notation_parser_db.grammars.level2_ast_grammar let term status = status#notation_parser_db.grammars.term let let_defs status = status#notation_parser_db.grammars.let_defs +let let_codefs status = status#notation_parser_db.grammars.let_codefs let protected_binder_vars status = status#notation_parser_db.grammars.protected_binder_vars diff --git a/matitaB/components/content_pres/cicNotationParser.mli b/matitaB/components/content_pres/cicNotationParser.mli index d711a3067..7ea722257 100644 --- a/matitaB/components/content_pres/cicNotationParser.mli +++ b/matitaB/components/content_pres/cicNotationParser.mli @@ -80,6 +80,9 @@ val term : #status -> NotationPt.term Grammar.Entry.e val let_defs : #status -> (NotationPt.term NotationPt.capture_variable list * NotationPt.term NotationPt.capture_variable * NotationPt.term * int) list Grammar.Entry.e +val let_codefs : #status -> + (NotationPt.term NotationPt.capture_variable list * NotationPt.term NotationPt.capture_variable * NotationPt.term * int) list + Grammar.Entry.e val protected_binder_vars : #status -> (NotationPt.term list * NotationPt.term option) Grammar.Entry.e diff --git a/matitaB/components/grafite/grafiteAst.ml b/matitaB/components/grafite/grafiteAst.ml index bc001d173..bda9e36e1 100644 --- a/matitaB/components/grafite/grafiteAst.ml +++ b/matitaB/components/grafite/grafiteAst.ml @@ -29,34 +29,36 @@ type direction = [ `LeftToRight | `RightToLeft ] type loc = Stdpp.location +type nterm = NotationPt.term + type npattern = - NotationPt.term option * (string * NotationPt.term) list * NotationPt.term option + nterm option * (string * nterm) list * nterm option -type auto_params = (bool * NotationPt.term list) option * (string*string) list +type auto_params = (bool * nterm list) option * (string*string) list type ntactic = - | NApply of loc * NotationPt.term - | NSmartApply of loc * NotationPt.term - | NAssert of loc * ((string * [`Decl of NotationPt.term | `Def of NotationPt.term * NotationPt.term]) list * NotationPt.term) list - | NCases of loc * NotationPt.term * npattern + | NApply of loc * nterm + | NSmartApply of loc * nterm + | NAssert of loc * ((string * [`Decl of nterm | `Def of nterm * nterm]) list * nterm) list + | NCases of loc * nterm * npattern | NCase1 of loc * string - | NChange of loc * npattern * NotationPt.term + | NChange of loc * npattern * nterm | NClear of loc * string list - | NConstructor of loc * int option * NotationPt.term list - | NCut of loc * NotationPt.term -(* | NDiscriminate of loc * NotationPt.term - | NSubst of loc * NotationPt.term *) + | NConstructor of loc * int option * nterm list + | NCut of loc * nterm +(* | NDiscriminate of loc * nterm + | NSubst of loc * nterm *) | NDestruct of loc * string list option * string list - | NElim of loc * NotationPt.term * npattern + | NElim of loc * nterm * npattern | NGeneralize of loc * npattern | NId of loc | NIntro of loc * string | NIntros of loc * string list - | NInversion of loc * NotationPt.term * npattern - | NLApply of loc * NotationPt.term - | NLetIn of loc * npattern * NotationPt.term * string + | NInversion of loc * nterm * npattern + | NLApply of loc * nterm + | NLetIn of loc * npattern * nterm * string | NReduce of loc * [ `Normalize of bool | `Whd of bool ] * npattern - | NRewrite of loc * direction * NotationPt.term * npattern + | NRewrite of loc * direction * nterm * npattern | NAuto of loc * auto_params | NDot of loc | NSemicolon of loc @@ -75,7 +77,7 @@ type ntactic = | NBlock of loc * ntactic list type nmacro = - | NCheck of loc * NotationPt.term + | NCheck of loc * nterm | Screenshot of loc * string | NAutoInteractive of loc * auto_params | NIntroGuess of loc @@ -96,21 +98,20 @@ type inclusion_mode = WithPreferences | WithoutPreferences | OnlyPreferences (* type command = | Include of loc * inclusion_mode * string (* _,buri,_,path *) - | UnificationHint of loc * NotationPt.term * int (* term, precedence *) - | NObj of loc * NotationPt.term NotationPt.obj - | NDiscriminator of loc * NotationPt.term - | NInverter of loc * string * NotationPt.term * bool list option * NotationPt.term option + | UnificationHint of loc * nterm * int (* term, precedence *) + | NObj of loc * nterm NotationPt.obj * bool + | NDiscriminator of loc * nterm + | NInverter of loc * string * nterm * bool list option * nterm option | NUnivConstraint of loc * NUri.uri * NUri.uri | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list - | NCoercion of loc * string * - (NotationPt.term * NotationPt.term * - (string * NotationPt.term) * NotationPt.term) option + | NCoercion of loc * string * bool * + (nterm * nterm * (string * nterm) * nterm) option | NQed of loc * bool (* ex lexicon commands *) | Alias of loc * alias_spec (** parameters, name, type, fields *) - | Notation of loc * direction option * NotationPt.term * Gramext.g_assoc * - int * NotationPt.term + | Notation of loc * direction option * nterm * Gramext.g_assoc * + int * nterm (* direction, l1 pattern, associativity, precedence, l2 pattern *) | Interpretation of loc * string * (string * NotationPt.argument_pattern list) * diff --git a/matitaB/components/grafite/grafiteAstPp.ml b/matitaB/components/grafite/grafiteAstPp.ml index d4d312bd2..62ffc2762 100644 --- a/matitaB/components/grafite/grafiteAstPp.ml +++ b/matitaB/components/grafite/grafiteAstPp.ml @@ -54,7 +54,7 @@ let pp_tactic_pattern status ~map_unicode_to_tex (what, hyp, goal) = let rec pp_ntactic status ~map_unicode_to_tex = let pp_tactic_pattern = pp_tactic_pattern ~map_unicode_to_tex in function - | NApply (_,t) -> "napply " ^ NotationPp.pp_term status t + | NApply (_,t) -> "@" ^ NotationPp.pp_term status t | NSmartApply (_,t) -> "fixme" | NAuto (_,(None,flgs)) -> "nautobatch" ^ @@ -166,8 +166,11 @@ let pp_ncommand status = function | NInverter (_,_,_,_,_) | NUnivConstraint (_) -> "not supported" | NCoercion (_) -> "not supported" - | NObj (_,obj) -> NotationPp.pp_obj (NotationPp.pp_term status) obj - | NQed (_,_) -> "nqed" + | NObj (_,obj,index) -> + (if not index then "-" else "") ^ + NotationPp.pp_obj (NotationPp.pp_term status) obj + | NQed (_,true) -> "qed" + | NQed (_,false) -> "qed-" | NCopy (_,name,uri,map) -> "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^ String.concat " and " @@ -176,9 +179,9 @@ let pp_ncommand status = function map) | Include (_,mode,path) -> (* not precise, since path is absolute *) if mode = WithPreferences then - "include \"" ^ path ^ "\"." + "include \"" ^ path ^ "\"" else - "include' \"" ^ path ^ "\"." + "include' \"" ^ path ^ "\"" | Alias (_,s) -> pp_alias s | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) -> pp_interpretation dsc symbol arg_patterns cic_appl_pattern diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml index 202111485..630d6a6e3 100644 --- a/matitaB/components/grafite_engine/grafiteEngine.ml +++ b/matitaB/components/grafite_engine/grafiteEngine.ml @@ -493,7 +493,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = GrafiteTypes.Serializer.require ~alias_only ~baseuri ~fname:fullpath status | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n - | GrafiteAst.NCoercion (loc, name, None) -> + | GrafiteAst.NCoercion (loc, name, compose, None) -> let status, t, ty, source, target = let o_t = NotationPt.Ident (name,`Ambiguous) in let metasenv,subst, status,t = @@ -514,13 +514,15 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = | _ -> assert false in aux ty in status, o_t, NotationPt.NCic ty, source, target in let status, composites = - NCicCoercDeclaration.eval_ncoercion status name t ty source target in + NCicCoercDeclaration.eval_ncoercion status name compose 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.NCoercion (loc, name, Some (t, ty, source, target)) -> + | GrafiteAst.NCoercion (loc, name, compose, Some (t, ty, source, target)) -> let status, composites = - NCicCoercDeclaration.eval_ncoercion status name t ty source target in + NCicCoercDeclaration.eval_ncoercion status name compose 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) @@ -544,7 +546,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = (match spec with | NReference.Def _ -> NReference.Def height | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height) - | NReference.CoFix _ -> NReference.CoFix height + | NReference.CoFix i -> NReference.CoFix i | NReference.Ind _ | NReference.Con _ | NReference.Decl as s -> s)) | t -> NCicUtils.map status (fun _ () -> ()) () fix t @@ -593,7 +595,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = try let nstatus = eval_ncommand ~include_paths opts status - ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml)) + ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml,true)) in if nstatus#ng_mode <> `CommandMode then begin @@ -611,9 +613,10 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = ) status boxml in let _,_,_,_,nobj = obj in let status = match nobj with - NCic.Inductive (is_ind,leftno,[it],_) -> - let _,ind_name,ty,cl = it in - List.fold_left + NCic.Inductive (is_ind,leftno,itl,_) -> + List.fold_left (fun status it -> + (let _,ind_name,ty,cl = it in + List.fold_left (fun status outsort -> let status = status#set_ng_mode `ProofMode in try @@ -633,7 +636,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = status (NCic.Prop:: List.map (fun s -> NCic.Type s) - (NCicEnvironment.get_universes status)) + (NCicEnvironment.get_universes status)))) status itl | _ -> status in let coercions = @@ -656,7 +659,8 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let status, nuris = NCicCoercDeclaration. basic_eval_and_record_ncoercion_from_t_cpos_arity - status (name,t,cpos,arity) in + + status (name,true,t,cpos,arity) in let aliases = GrafiteDisambiguate.aliases_for_objs status nuris in eval_alias status (mode,aliases) with GrafiteDisambiguate.Error _ -> @@ -700,7 +704,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let status = subst_metasenv_and_fix_names status in let status = status#set_ng_mode `ProofMode in eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,false)) - | GrafiteAst.NObj (loc,obj) -> + | GrafiteAst.NObj (loc,obj,index) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") else @@ -715,26 +719,30 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let status = status#set_ng_mode `ProofMode in (match nmenv with [] -> - eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,true)) + eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed + (Stdpp.dummy_loc,index)) | _ -> status) - | GrafiteAst.NDiscriminator (_,_) -> assert false (*(loc, indty) -> + | GrafiteAst.NDiscriminator (loc, indty) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") else let status = status#set_ng_mode `ProofMode in let metasenv,subst,status,indty = - GrafiteDisambiguate.disambiguate_nterm None status [] [] [] (text,prefix_len,indty) in - let indtyno, (_,_,tys,_,_) = match indty with - NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,_))) as r) -> - indtyno, NCicEnvironment.get_checked_indtys r + GrafiteDisambiguate.disambiguate_nterm status None [] [] [] (text,prefix_len,indty) in + let indtyno, (_,_,tys,_,_), leftno = match indty with + NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,leftno))) as r) -> + indtyno, NCicEnvironment.get_checked_indtys status r, leftno | _ -> prerr_endline ("engine: indty expected... (fix this error message)"); assert false in - let it = List.nth tys indtyno in - let status,obj = NDestructTac.mk_discriminator it status in + let (_,ind_name,_,_ as it) = List.nth tys indtyno in + let status,obj = + NDestructTac.mk_discriminator ~use_jmeq:true (ind_name ^ "_jmdiscr") + it leftno status status#baseuri in let _,_,menv,_,_ = obj in (match menv with - [] -> eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) + [] -> eval_ncommand ~include_paths opts status + ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false)) | _ -> prerr_endline ("Discriminator: non empty metasenv"); - status, []) *) + status) | GrafiteAst.NInverter (loc, name, indty, selection, sort) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") @@ -776,7 +784,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = (match menv with [] -> eval_ncommand ~include_paths opts status - ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,false)) + ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false)) | _ -> assert false) | GrafiteAst.NUnivConstraint (loc,u1,u2) -> eval_add_constraint status [`Type,u1] [`Type,u2] diff --git a/matitaB/components/grafite_engine/nCicCoercDeclaration.ml b/matitaB/components/grafite_engine/nCicCoercDeclaration.ml index 52b074c4a..03e3f87e1 100644 --- a/matitaB/components/grafite_engine/nCicCoercDeclaration.ml +++ b/matitaB/components/grafite_engine/nCicCoercDeclaration.ml @@ -262,11 +262,11 @@ let close_graph name t s d to_s from_d p a status = ;; (* idempotent *) -let basic_index_ncoercion (name,t,s,d,position,arity) status = +let basic_index_ncoercion (name,_compose,t,s,d,position,arity) status = NCicCoercion.index_coercion status name t s d arity position ;; -let basic_eval_ncoercion (name,t,s,d,p,a) status = +let basic_eval_ncoercion (name,compose,t,s,d,p,a) status = let to_s = NCicCoercion.look_for_coercion status [] [] [] skel_dummy s in @@ -274,10 +274,11 @@ let basic_eval_ncoercion (name,t,s,d,p,a) status = NCicCoercion.look_for_coercion status [] [] [] d skel_dummy in let status = NCicCoercion.index_coercion status name t s d a p in - let composites = close_graph name t s d to_s from_d p a status in + let composites = + if compose then close_graph name t s d to_s from_d p a status else [] in List.fold_left (fun (uris,infos,st) ((uri,_,_,_,_ as obj),name,t,s,d,p,a) -> - let info = name,t,s,d,p,a in + let info = name,compose,t,s,d,p,a in let st = NCicLibrary.add_obj st obj in let st = basic_index_ncoercion info st in uri::uris, info::infos, st) @@ -285,19 +286,17 @@ let basic_eval_ncoercion (name,t,s,d,p,a) status = ;; let record_ncoercion = - let aux (name,t,s,d,p,a) ~refresh_uri_in_term = + let aux (name,compose,t,s,d,p,a) ~refresh_uri_in_term = let t = refresh_uri_in_term t in let s = refresh_uri_in_term s in let d = refresh_uri_in_term d in - basic_index_ncoercion (name,t,s,d,p,a) + basic_index_ncoercion (name,compose,t,s,d,p,a) in let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference ~alias_only status = if not alias_only then - List.fold_right - (aux ~refresh_uri_in_term:(refresh_uri_in_term - (status:>NCicEnvironment.status))) l status + List.fold_right (aux ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCicEnvironment.status))) l status else status in @@ -310,17 +309,17 @@ let basic_eval_and_record_ncoercion infos status = ;; let basic_eval_and_record_ncoercion_from_t_cpos_arity - status (name,t,cpos,arity) + status (name,compose,t,cpos,arity) = let ty = NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] [] t in let src,tgt = src_tgt_of_ty_cpos_arity status ty cpos arity in let status, uris = - basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status + basic_eval_and_record_ncoercion (name,compose,t,src,tgt,cpos,arity) status in status,uris ;; -let eval_ncoercion (status: #GrafiteTypes.status) name t ty (id,src) tgt = +let eval_ncoercion (status: #GrafiteTypes.status) name compose t ty (id,src) tgt = let metasenv,subst,status,ty = GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in assert (metasenv=[]); @@ -332,7 +331,7 @@ let eval_ncoercion (status: #GrafiteTypes.status) name t ty (id,src) tgt = let status, src, tgt, cpos, arity = src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in let status, uris = - basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status + basic_eval_and_record_ncoercion (name,compose,t,src,tgt,cpos,arity) status in status,uris ;; diff --git a/matitaB/components/grafite_engine/nCicCoercDeclaration.mli b/matitaB/components/grafite_engine/nCicCoercDeclaration.mli index 9bca1143d..11119fe82 100644 --- a/matitaB/components/grafite_engine/nCicCoercDeclaration.mli +++ b/matitaB/components/grafite_engine/nCicCoercDeclaration.mli @@ -14,6 +14,7 @@ val eval_ncoercion: #GrafiteTypes.status as 'status -> string -> + bool -> NotationPt.term -> NotationPt.term -> string * NotationPt.term -> @@ -24,5 +25,5 @@ val eval_ncoercion: * the arity in the `:arity>` syntax *) val basic_eval_and_record_ncoercion_from_t_cpos_arity: #GrafiteTypes.status as 'status -> - string * NCic.term * int * int -> 'status * NUri.uri list + string * bool * NCic.term * int * int -> 'status * NUri.uri list diff --git a/matitaB/components/grafite_parser/grafiteParser.ml b/matitaB/components/grafite_parser/grafiteParser.ml index b72fecb76..7985512d9 100644 --- a/matitaB/components/grafite_parser/grafiteParser.ml +++ b/matitaB/components/grafite_parser/grafiteParser.ml @@ -72,9 +72,9 @@ let mk_rec_corec ind_kind defs loc = let body = N.Ident (name,`Ambiguous) in (loc, N.Theorem(`Definition, name, ty, Some (N.LetRec (ind_kind, defs, body)), `Regular)) -let nmk_rec_corec ind_kind defs loc = +let nmk_rec_corec ind_kind defs loc index = let loc,t = mk_rec_corec ind_kind defs loc in - G.NObj (loc,t) + G.NObj (loc,t,index) (* let nnon_punct_of_punct = function @@ -93,27 +93,18 @@ let mk_parser statement lstatus = (* let grammar = CicNotationParser.level2_ast_grammar lstatus in *) let term = CicNotationParser.term lstatus in let let_defs = CicNotationParser.let_defs lstatus in + let let_codefs = CicNotationParser.let_codefs lstatus in let protected_binder_vars = CicNotationParser.protected_binder_vars lstatus in (* {{{ parser initialization *) EXTEND GLOBAL: term statement; constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ]; tactic_term: [ [ t = term LEVEL "90" -> t ] ]; -(* MATITA 1.0 - new_name: [ - [ SYMBOL "_" -> None - | id = IDENT -> Some id ] - ]; -*) ident_list1: [ [ LPAREN; idents = LIST1 IDENT; RPAREN -> idents ] ]; - tactic_term_list1: [ - [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ] - ]; nreduction_kind: [ [ IDENT "normalize" ; delta = OPT [ IDENT "nodelta" -> () ] -> let delta = match delta with None -> true | _ -> false in `Normalize delta - (*| IDENT "unfold"; t = OPT tactic_term -> `Unfold t*) | IDENT "whd" ; delta = OPT [ IDENT "nodelta" -> () ] -> let delta = match delta with None -> true | _ -> false in `Whd delta] @@ -143,7 +134,8 @@ EXTEND Some wanted,sps | sps = sequent_pattern_spec -> None,Some sps - ] -> + ]; + SYMBOL ";" -> let wanted,hyp_paths,goal_path = match wanted_and_sps with wanted,None -> wanted, [], Some N.UserInput @@ -177,19 +169,8 @@ EXTEND | SYMBOL "<" -> `RightToLeft ] ]; int: [ [ num = NUMBER -> int_of_string num ] ]; -(* MATITA 1.0 - intros_spec: [ - [ OPT [ IDENT "names" ]; - num = OPT [ num = int -> num ]; - idents = intros_names -> - num, idents - ] - ]; -*) -(* MATITA 1.0 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ]; *) ntactic: [ [ SYMBOL "@"; t = tactic_term -> G.NTactic(loc,[G.NApply (loc, t)]) - | IDENT "apply"; t = tactic_term -> G.NTactic(loc,[G.NApply (loc, t)]) | IDENT "applyS"; t = tactic_term -> G.NTactic(loc,[G.NSmartApply(loc, t)]) | IDENT "assert"; seqs = LIST0 [ @@ -201,8 +182,6 @@ EXTEND SYMBOL <:unicode>; concl = tactic_term -> (List.rev hyps,concl) ] -> G.NTactic(loc,[G.NAssert (loc, seqs)]) - (*| IDENT "auto"; params = auto_params -> - G.NTactic(loc,[G.NAuto (loc, params)])*) | SYMBOL "/"; num = OPT NUMBER ; just_and_params = auto_params; SYMBOL "/" -> let just,params = just_and_params in @@ -214,28 +193,23 @@ EXTEND | Some (b,`Univ univ) -> G.NTactic(loc, [G.NAuto(loc,(Some (b,univ),["depth",depth]@params))]) - | Some (b,`EmptyUniv) -> - G.NTactic(loc, - [G.NAuto(loc,(Some (b,[]),["depth",depth]@params))]) | Some (b,`Trace) -> G.NMacro(loc, G.NAutoInteractive (loc, (None,["depth",depth]@params)))) - | IDENT "intros" -> G.NMacro (loc, G.NIntroGuess loc) + | SYMBOL "#"; SYMBOL "#" -> G.NMacro (loc, G.NIntroGuess loc) | IDENT "check"; t = tactic_term -> G.NMacro(loc,G.NCheck (loc,t)) | IDENT "screenshot"; fname = QSTRING -> G.NMacro(loc,G.Screenshot (loc, fname)) | IDENT "cases"; what = tactic_term ; where = pattern_spec -> G.NTactic(loc,[G.NCases (loc, what, where)]) - | IDENT "change"; what = pattern_spec; "with"; with_what = tactic_term -> + | IDENT "change"; "with"; with_what = tactic_term; what = pattern_spec -> G.NTactic(loc,[G.NChange (loc, what, with_what)]) - | SYMBOL "-"; ids = LIST1 IDENT -> - G.NTactic(loc,[G.NClear (loc, ids)]) - | (*SYMBOL "^"*)PLACEHOLDER; num = OPT NUMBER; + | SYMBOL "-"; id = IDENT -> + G.NTactic(loc,[G.NClear (loc, [id])]) + | PLACEHOLDER; num = OPT NUMBER; l = OPT [ SYMBOL "{"; l = LIST1 tactic_term; SYMBOL "}" -> l ] -> G.NTactic(loc,[G.NConstructor (loc, (match num with None -> None | Some x -> Some (int_of_string x)),match l with None -> [] | Some l -> l)]) | IDENT "cut"; t = tactic_term -> G.NTactic(loc,[G.NCut (loc, t)]) -(* | IDENT "discriminate"; t = tactic_term -> G.NDiscriminate (loc, t) - | IDENT "subst"; t = tactic_term -> G.NSubst (loc, t) *) | IDENT "destruct"; just = OPT [ dom = ident_list1 -> dom ]; exclude = OPT [ IDENT "skip"; skip = ident_list1 -> skip ] -> let exclude' = match exclude with None -> [] | Some l -> l in @@ -254,8 +228,6 @@ EXTEND G.NTactic(loc,[G.NReduce (loc, kind, p)]) | dir = direction; what = tactic_term ; where = pattern_spec -> G.NTactic(loc,[G.NRewrite (loc, dir, what, where)]) - | IDENT "rewrite"; dir = direction; what = tactic_term ; where = pattern_spec -> - G.NTactic(loc,[G.NRewrite (loc, dir, what, where)]) | IDENT "try"; tac = SELF -> let tac = match tac with G.NTactic(_,[t]) -> t | _ -> assert false in G.NTactic(loc,[ G.NTry (loc,tac)]) @@ -271,20 +243,15 @@ EXTEND | SYMBOL "#"; ns=IDENT -> G.NTactic(loc,[ G.NIntros (loc,[ns])]) | SYMBOL "#"; SYMBOL "_" -> G.NTactic(loc,[ G.NIntro (loc,"_")]) | SYMBOL "*" -> G.NTactic(loc,[ G.NCase1 (loc,"_")]) - | SYMBOL "*"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)]) + | SYMBOL "*"; "as"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)]) ] ]; auto_fixed_param: [ [ IDENT "demod" | IDENT "fast_paramod" | IDENT "paramod" - | IDENT "depth" | IDENT "width" | IDENT "size" - | IDENT "timeout" - | IDENT "library" - | IDENT "type" - | IDENT "all" ] ]; auto_params: [ @@ -297,8 +264,7 @@ EXTEND [ IDENT "by" -> true | IDENT "trace" -> false ]; by = - [ univ = tactic_term_list1 -> `Univ univ - | SYMBOL "{"; SYMBOL "}" -> `EmptyUniv + [ univ = LIST0 tactic_term SEP SYMBOL "," -> `Univ univ | SYMBOL "_" -> `Trace ] -> is_user_trace,by ] -> just,params ] ]; @@ -538,36 +504,39 @@ EXTEND loc,path,G.WithoutPreferences ]]; + index: [[ b = OPT SYMBOL "-" -> match b with None -> true | _ -> false ]]; + grafite_ncommand: [ [ - IDENT "qed" ; b = OPT SYMBOL "-" -> - let b = match b with None -> true | Some _ -> false in G.NQed (loc,b) + IDENT "qed" ; i = index -> G.NQed (loc,i) | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> - G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular)) + G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular),true) | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode> (* ≝ *); body = term -> - G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body,`Regular)) - | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term -> - G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular)) + G.NObj (loc, + N.Theorem(nflavour, name, N.Implicit `JustOne, Some body,`Regular), + true) + | IDENT "axiom"; i = index; name = IDENT; SYMBOL ":"; typ = term -> + G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular),i) | IDENT "discriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty) | IDENT "inverter"; name = IDENT; IDENT "for" ; indty = tactic_term ; paramspec = OPT inverter_param_list ; outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] -> G.NInverter (loc,name,indty,paramspec,outsort) - | LETCOREC ; defs = let_defs -> - nmk_rec_corec `CoInductive defs loc + | LETCOREC ; defs = let_codefs -> + nmk_rec_corec `CoInductive defs loc true | LETREC ; defs = let_defs -> - nmk_rec_corec `Inductive defs loc + nmk_rec_corec `Inductive defs loc true | IDENT "inductive"; spec = inductive_spec -> let (params, ind_types) = spec in - G.NObj (loc, N.Inductive (params, ind_types)) + G.NObj (loc, N.Inductive (params, ind_types),true) | IDENT "coinductive"; spec = inductive_spec -> let (params, ind_types) = spec in let ind_types = (* set inductive flags to false (coinductive) *) List.map (fun (name, _, term, ctors) -> (name, false, term, ctors)) ind_types in - G.NObj (loc, N.Inductive (params, ind_types)) + G.NObj (loc, N.Inductive (params, ind_types),true) | IDENT "universe"; IDENT "constraint"; u1 = tactic_term; SYMBOL <:unicode> ; u2 = tactic_term -> let urify = function @@ -580,13 +549,16 @@ EXTEND G.NUnivConstraint (loc,u1,u2) | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term -> G.UnificationHint (loc, t, n) - | IDENT "coercion"; name = IDENT; spec = OPT [ SYMBOL ":"; ty = term; + | IDENT "coercion"; name = IDENT; + compose = OPT [ IDENT "nocomposites" -> () ]; + spec = OPT [ SYMBOL ":"; ty = term; SYMBOL <:unicode>; t = term; "on"; id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term; "to"; target = term -> t,ty,(id,source),target ] -> - G.NCoercion(loc,name,spec) + let compose = compose = None in + G.NCoercion(loc,name,compose,spec) | IDENT "record" ; (params,name,ty,fields) = record_spec -> - G.NObj (loc, N.Record (params,name,ty,fields)) + G.NObj (loc, N.Record (params,name,ty,fields),true) | IDENT "copy" ; s = IDENT; IDENT "from"; u = URI; "with"; m = LIST0 [ u1 = URI; SYMBOL <:unicode>; u2 = URI -> u1,u2 ] -> G.NCopy (loc,s,NUri.uri_of_string u, diff --git a/matitaB/components/ng_kernel/nCic.ml b/matitaB/components/ng_kernel/nCic.ml index 271bf5284..c08f4ed04 100644 --- a/matitaB/components/ng_kernel/nCic.ml +++ b/matitaB/components/ng_kernel/nCic.ml @@ -94,6 +94,7 @@ type def_pragma = (* pragmatic of the object *) | `Elim of sort (* elimination principle; universe is not relevant *) | `Projection (* record projection *) | `InversionPrinciple (* inversion principle *) + | `DiscriminationPrinciple (* discrimination principle *) | `Variant | `Local | `Regular ] (* Local = hidden technicality *) diff --git a/matitaB/components/ng_kernel/nCicPp.ml b/matitaB/components/ng_kernel/nCicPp.ml index 80eb372ae..d19914ab4 100644 --- a/matitaB/components/ng_kernel/nCicPp.ml +++ b/matitaB/components/ng_kernel/nCicPp.ml @@ -280,6 +280,7 @@ let string_of_pragma = function | `Elim _sort -> "Elim _" | `Projection -> "Projection" | `InversionPrinciple -> "InversionPrinciple" + | `DiscriminationPrinciple -> "DiscriminationPrinciple" | `Variant -> "Variant" | `Local -> "Local" | `Regular -> "Regular" diff --git a/matitaB/components/ng_tactics/nDestructTac.ml b/matitaB/components/ng_tactics/nDestructTac.ml index ef564afc6..dcd774994 100644 --- a/matitaB/components/ng_tactics/nDestructTac.ml +++ b/matitaB/components/ng_tactics/nDestructTac.ml @@ -44,6 +44,8 @@ let mk_id id = NotationPt.Ident (id,`Ambiguous) ;; +let mk_sym s = NotationPt.Symbol (s,None);; + let rec mk_prods l t = match l with [] -> t @@ -71,6 +73,14 @@ let subst_metasenv_and_fix_names status = status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv status subst metasenv,subst,o) ;; +(* needed to workaround a weakness of the refiner? *) +let rec generalize0_tac tl s = + match tl with + | [] -> s + | t0::tl0 -> NTactics.generalize0_tac [t0] (generalize0_tac tl0 s) +;; + + (* input: nome della variabile riscritta * output: lista dei nomi delle variabili il cui tipo dipende dall'input *) let cascade_select_in_ctx status ~subst ctx skip iname = @@ -125,11 +135,55 @@ let nargs it nleft consno = List.length (arg_list nleft t_k) ;; let default_pattern = "",0,(None,[],Some NotationPt.UserInput);; +let prod_pattern = + "",0,(None,[],Some NotationPt.Binder + (`Pi, (mk_id "_",Some (NotationPt.Appl + [ NotationPt.Implicit `JustOne + ; NotationPt.Implicit `JustOne + ; NotationPt.UserInput + ; NotationPt.Implicit `JustOne ])), + NotationPt.Implicit `JustOne));; + +let prod_pattern_jm = + "",0,(None,[],Some NotationPt.Binder + (`Pi, (mk_id "_",Some (NotationPt.Appl + [ NotationPt.Implicit `JustOne + ; NotationPt.Implicit `JustOne + ; NotationPt.UserInput + ; NotationPt.Implicit `JustOne + ; NotationPt.Implicit `JustOne ])), + NotationPt.Implicit `JustOne));; + +let hp_pattern n = + "",0,(None,[n, NotationPt.Appl + [ NotationPt.Implicit `JustOne + ; NotationPt.Implicit `JustOne + ; NotationPt.UserInput + ; NotationPt.Implicit `JustOne ] ], + None);; + +let hp_pattern_jm n = + "",0,(None,[n, NotationPt.Appl + [ NotationPt.Implicit `JustOne + ; NotationPt.Implicit `JustOne + ; NotationPt.UserInput + ; NotationPt.Implicit `JustOne + ; NotationPt.Implicit `JustOne ] ], + None);; + +exception ConstructorTooBig of string;; (* returns the discrimination = injection+contradiction principle *) -let mk_discriminator it ~use_jmeq nleft xyty status = - let _,indname,_,cl = it in +let mk_discriminator ~use_jmeq name it leftno status baseuri = + let itnargs = + let _,_,arity,_ = it in + List.length (arg_list 0 arity) in + let _,itname,_,_ = it in + let params = List.map (fun x -> "a" ^ string_of_int x) (HExtlib.list_seq 1 (itnargs+1)) in + let xyty = mk_appl (List.map mk_id (itname::params)) in + + (* PHASE 1: derive the type of the discriminator (we'll name it "principle") *) let mk_eq tys ts us es n = @@ -157,15 +211,16 @@ let mk_discriminator it ~use_jmeq nleft xyty status = List.nth us n] in + + let _,_,_,cl = it in - let kname it j = - let _,_,_,cl = it in + let kname (*it*) j = let _,name,_ = List.nth cl j in name in let branch i j ts us = - let nargs = nargs it nleft i in + let nargs = nargs it leftno i in let es = List.map (fun x -> mk_id ("e" ^ string_of_int x)) (HExtlib.list_seq 0 nargs) in let tys = List.map (fun x -> iter @@ -181,10 +236,10 @@ let mk_discriminator it ~use_jmeq nleft xyty status = NotationPt.Binder (`Lambda, (mk_id ("p" ^ string_of_int i), None), acc))) (nargs-1) (mk_appl [mk_id "eq"; NotationPt.Implicit `JustOne; - mk_appl (mk_id (kname it i):: + mk_appl (mk_id (kname i):: List.map (fun x -> mk_id ("x" ^string_of_int x)) (HExtlib.list_seq 0 (List.length ts))); - mk_appl (mk_id (kname it j)::us)])] + mk_appl (mk_id (kname j)::us)])] in (** NotationPt.Binder (`Lambda, (mk_id "e", Some (mk_appl @@ -221,12 +276,12 @@ let mk_discriminator it ~use_jmeq nleft xyty status = None, List.map (fun j -> - let nargs_kty = nargs it nleft j in + let nargs_kty = nargs it leftno j in let us = iter (fun m acc -> mk_id ("u" ^ (string_of_int m))::acc) (nargs_kty - 1) [] in let nones = iter (fun _ acc -> None::acc) (nargs_kty - 1) [] in - NotationPt.Pattern (kname it j, + NotationPt.Pattern (kname j, None, List.combine us nones), branch i j ts us) @@ -237,47 +292,58 @@ let mk_discriminator it ~use_jmeq nleft xyty status = None , List.map (fun i -> - let nargs_kty = nargs it nleft i in + let nargs_kty = nargs it leftno i in + if (nargs_kty > 5 && not use_jmeq) then raise (ConstructorTooBig (kname i)); let ts = iter (fun m acc -> mk_id ("t" ^ (string_of_int m))::acc) (nargs_kty - 1) [] in let nones = iter (fun _ acc -> None::acc) (nargs_kty - 1) [] in - NotationPt.Pattern (kname it i, + NotationPt.Pattern (kname i, None, List.combine ts nones), inner i ts) (HExtlib.list_seq 0 (List.length cl))) in - let principle = NotationPt.Binder (`Lambda, (mk_id "x", Some xyty), - NotationPt.Binder (`Lambda, (mk_id "y", Some xyty), outer)) + let principle = + mk_prods params (NotationPt.Binder (`Forall, (mk_id "x", + Some xyty), + NotationPt.Binder (`Forall, (mk_id "y", Some xyty), + (if use_jmeq then + NotationPt.Binder (`Forall, (mk_id "e", + Some (mk_appl + [mk_sym "jmsimeq"; NotationPt.Implicit `JustOne; mk_id "x"; + NotationPt.Implicit `JustOne; mk_id "y"])), + outer) + else + NotationPt.Binder (`Forall, (mk_id "e", + Some (mk_appl [mk_sym "eq";NotationPt.Implicit `JustOne; mk_id "x"; mk_id "y"])), + outer))))) in pp (lazy ("discriminator = " ^ (NotationPp.pp_term status principle))); - - status, principle -;; - -let hd_of_term = function - | NCic.Appl (hd::_) -> hd - | t -> t -;; - -let name_of_rel ~context rel = - let s, _ = List.nth context (rel-1) in s -;; - -(* let lookup_in_ctx ~context n = - List.nth context ((List.length context) - n - 1) -;;*) - -let discriminate_tac ~context cur_eq status = - pp (lazy (Printf.sprintf "discriminate: equation %s" (name_of_rel ~context cur_eq))); + (* PHASE 2: create the object for the proof of the principle: we'll name it + * "theorem" *) + let status, theorem = + GrafiteDisambiguate.disambiguate_nobj status ~baseuri + (baseuri ^ name ^ ".def",0, + NotationPt.Theorem + (`Theorem,name,principle, + Some (NotationPt.Implicit (`Tagged "inv")),`DiscriminationPrinciple)) + in + let uri,height,nmenv,nsubst,nobj = theorem in + let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in + let status = status#set_obj theorem in + let status = status#set_stack ninitial_stack in + let status = subst_metasenv_and_fix_names status in + + (* PHASE 3: we finally prove the discrimination principle *) let dbranch it ~use_jmeq leftno consno = - let refl_id = mk_id (if use_jmeq then "refl_jmeq" else "refl") in + let refl_id = mk_sym "refl" in pp (lazy (Printf.sprintf "dbranch %d %d" leftno consno)); let nlist = HExtlib.list_seq 0 (nargs it leftno consno) in (* (\forall ...\forall P.\forall DH : ( ... = ... -> P). P) *) let params = List.map (fun x -> NTactics.intro_tac ("a" ^ string_of_int x)) nlist in - NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern:: + (* NTactics.reduce_tac ~reduction:(`Normalize true) + * ~where:default_pattern::*) params @ [ NTactics.intro_tac "P"; NTactics.intro_tac "DH"; @@ -286,7 +352,6 @@ let discriminate_tac ~context cur_eq status = ] in let dbranches it ~use_jmeq leftno = pp (lazy (Printf.sprintf "dbranches %d" leftno)); - let _,_,_,cl = it in let nbranches = List.length cl in let branches = iter (fun n acc -> let m = nbranches - n - 1 in @@ -298,15 +363,51 @@ let discriminate_tac ~context cur_eq status = NTactics.branch_tac ~force:false:: branches @ [NTactics.merge_tac] else branches in + let print_tac s status = pp s ; status in + + let status = + NTactics.block_tac ( + [print_tac (lazy "ci sono") (*; + NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern *) + ] + @ List.map (fun x -> NTactics.intro_tac x) params @ + [NTactics.intro_tac "x"; + NTactics.intro_tac "y"; + NTactics.intro_tac "Deq"; + print_tac (lazy "ci sono 2"); + NTactics.rewrite_tac ~dir:`RightToLeft ~what:("",0,mk_id "Deq") ~where:default_pattern; + NTactics.cases_tac ~what:("",0,mk_id "x") ~where:default_pattern] + @ dbranches it ~use_jmeq leftno) status + in status, status#obj +;; + +let hd_of_term status t = + match (snd (term_of_cic_term status + (snd (whd status (ctx_of t) t)) (ctx_of t))) with + | NCic.Appl (hd::_) -> hd + | t -> t +;; + +let name_of_rel ~context rel = + let s, _ = List.nth context (rel-1) in s +;; + +(* let lookup_in_ctx ~context n = + List.nth context ((List.length context) - n - 1) +;;*) + +let discriminate_tac ~context cur_eq status = + pp (lazy (Printf.sprintf "discriminate: equation %s" (name_of_rel ~context cur_eq))); + let eq_name,(NCic.Decl s | NCic.Def (s,_)) = List.nth context (cur_eq-1) in let _,ctx' = HExtlib.split_nth cur_eq context in let status, s = NTacStatus.whd status ctx' (mk_cic_term ctx' s) in let status, s = term_of_cic_term status s ctx' in - let status, leftno, it, use_jmeq = - let it, t1, t2, use_jmeq = match s with - | NCic.Appl [_;it;t1;t2] -> it,t1,t2,false - | NCic.Appl [_;it;t1;_;t2] -> it,t1,t2,true + let status,it,use_jmeq = + let it, use_jmeq = match s with + | NCic.Appl [_;it;_;_] -> it,false + | NCic.Appl [_;it;_;_;_] -> it,true | _ -> assert false in (* XXX: serve? ho già fatto whd *) let status, it = whd status ctx' (mk_cic_term ctx' it) in @@ -318,8 +419,8 @@ let discriminate_tac ~context cur_eq status = uri, indtyno, NCicEnvironment.get_checked_indtys status r | _ -> pp (lazy ("discriminate: indty =" ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] it)) ; assert false in - let _,leftno,its,_,_ = its in - status, leftno, List.nth its indtyno, use_jmeq + let _,_,its,_,_ = its in + status,List.nth its indtyno, use_jmeq in let itnargs = @@ -327,41 +428,16 @@ let discriminate_tac ~context cur_eq status = List.length (arg_list 0 arity) in let _,itname,_,_ = it in let params = List.map (fun x -> "a" ^ string_of_int x) (HExtlib.list_seq 1 (itnargs+1)) in - let xyty = mk_appl (List.map mk_id (itname::params)) in - let print_tac s status = pp s ; status in - NTactics.block_tac ( - [(fun status -> - let status, discr = mk_discriminator it ~use_jmeq leftno xyty status in - let cut_term = mk_prods params (NotationPt.Binder (`Forall, (mk_id "x", - Some xyty), - NotationPt.Binder (`Forall, (mk_id "y", Some xyty), - NotationPt.Binder (`Forall, (mk_id "e", - Some (mk_appl [mk_id "eq";NotationPt.Implicit `JustOne; mk_id "x"; mk_id "y"])), - mk_appl [discr; mk_id "x"; mk_id "y"(*;mk_id "e"*)])))) in - let status = print_tac (lazy ("cut_term = "^ NotationPp.pp_term status cut_term)) status in - NTactics.cut_tac ("",0, cut_term) - status); - NTactics.branch_tac; - print_tac (lazy "ci sono"); - NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern] - @ List.map (fun x -> NTactics.intro_tac x) params @ - [NTactics.intro_tac "x"; - NTactics.intro_tac "y"; - NTactics.intro_tac "Deq"; - print_tac (lazy "ci sono 2"); - NTactics.rewrite_tac ~dir:`RightToLeft ~what:("",0,mk_id "Deq") ~where:default_pattern; - NTactics.cases_tac ~what:("",0,mk_id "x") ~where:default_pattern] - @ dbranches it ~use_jmeq leftno @ - [NTactics.shift_tac; - print_tac (lazy "ci sono 3"); - NTactics.intro_tac "#discriminate"; - NTactics.apply_tac ("",0,mk_appl ([mk_id "#discriminate"]@ + let principle_name = + if use_jmeq then itname ^ "_jmdiscr" + else itname ^ "_discr" + in + pp (lazy ("apply (" ^ principle_name ^ " " ^ + (String.concat "" (HExtlib.mk_list "?" (List.length params + 2))) ^ + " " ^ eq_name ^ ")")); + NTactics.apply_tac ("",0,mk_appl ([mk_id principle_name]@ HExtlib.mk_list (NotationPt.Implicit `JustOne) (List.length params + 2) @ - [mk_id eq_name ])); - NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern; - NTactics.clear_tac ["#discriminate"]; - NTactics.merge_tac; print_tac (lazy "the end of discriminate")] - ) status + [mk_id eq_name ])) status ;; let saturate_skip status context skip = @@ -397,20 +473,38 @@ let subst_tac ~context ~dir skip cur_eq = | NCic.Rel var -> cascade_select_in_ctx status ~subst:(get_subst status) context skip (var+cur_eq) | _ -> cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in + let varname = match var with + | NCic.Rel var -> + let name,_ = List.nth context (var+cur_eq-1) in + HLog.warn (Printf.sprintf "destruct: trying to remove variable: %s" name); + [name] + | _ -> [] + in let names_to_gen = List.filter (fun n -> n <> eq_name) names_to_gen in if (List.exists (fun x -> List.mem x skip) names_to_gen) then oldstatus else - let gen_tac x = - NTactics.generalize_tac - ~where:("",0,(Some (mk_id x),[], Some NotationPt.UserInput)) in - NTactics.block_tac ((List.map gen_tac names_to_gen)@ - [NTactics.clear_tac names_to_gen; + let gen_tac x = + (fun s -> + let x' = String.concat " " x in + let x = List.map mk_id x in + (* let s = NTactics.print_tac false ("@generalize " ^ x') s in *) + generalize0_tac x s) in + NTactics.block_tac ( + (* (List.map gen_tac names_to_gen)@ *) + [gen_tac (List.rev names_to_gen); + NTactics.clear_tac names_to_gen; NTactics.rewrite_tac ~dir ~what:("",0,mk_id eq_name) ~where:default_pattern; - NTactics.reduce_tac ~reduction:(`Normalize true) - ~where:default_pattern; - NTactics.try_tac (NTactics.clear_tac [eq_name])]@ +(* NTactics.reduce_tac ~reduction:(`Normalize true) + ~where:default_pattern;*) + (* XXX: temo che la clear multipla funzioni bene soltanto se + * gli identificatori sono nell'ordine giusto. + * Per non saper né leggere né scrivere, usiamo due clear + * invece di una *) + NTactics.try_tac (NTactics.clear_tac [eq_name]); + NTactics.try_tac (NTactics.clear_tac varname); +]@ (List.map NTactics.intro_tac (List.rev names_to_gen))) status ;; @@ -421,91 +515,62 @@ let clearid_tac ~context skip cur_eq = let status, s = NTacStatus.whd status ctx' (mk_cic_term ctx' s) in let status, s = term_of_cic_term status s ctx' in let skip = saturate_skip status context skip in - (* - let streicher_id = - match s with - | NCic.Appl [_;_;_;_] -> mk_id "streicherK" - | NCic.Appl [_;_;_;_;_] -> mk_id "streicherKjmeq" - | _ -> assert false - in - pp (lazy (Printf.sprintf "clearid: equation %s" eq_name)); - let names_to_gen, _ = - cascade_select_in_ctx ~subst:(get_subst status) context cur_eq in - let names_to_gen = names_to_gen @ [eq_name] in - let gen_tac x = - NTactics.generalize_tac - ~where:("",0,(Some (mk_id x),[], Some NotationPt.UserInput)) in - NTactics.block_tac ((List.map gen_tac names_to_gen)@ - [NTactics.clear_tac names_to_gen; - NTactics.apply_tac ("",0, mk_appl [streicher_id; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne]); - NTactics.reduce_tac ~reduction:(`Normalize true) - ~where:default_pattern] @ - (let names_to_intro = - match List.rev names_to_gen with - | [] -> [] - | _::tl -> tl in - List.map NTactics.intro_tac names_to_intro)) status -*) pp (lazy (Printf.sprintf "clearid: equation %s" eq_name)); - match s with - | NCic.Appl [_;_;_;_] -> - (* leibniz *) - let streicher_id = mk_id "streicherK" - in - let names_to_gen, _ = - cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in - let names_to_gen = names_to_gen @ [eq_name] in - let gen_tac x = - NTactics.generalize_tac - ~where:("",0,(Some (mk_id x),[], Some NotationPt.UserInput)) in - NTactics.block_tac ((List.map gen_tac names_to_gen)@ - [NTactics.clear_tac names_to_gen; - NTactics.apply_tac ("",0, mk_appl [streicher_id; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne]); - NTactics.reduce_tac ~reduction:(`Normalize true) - ~where:default_pattern] @ - (let names_to_intro = - match List.rev names_to_gen with - | [] -> [] - | _::tl -> tl in - List.map NTactics.intro_tac names_to_intro)) status - | NCic.Appl [_;_;_;_;_] -> - (* JMeq *) - let streicher_id = mk_id "streicherK" - in - let names_to_gen, _ = - cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in - let names_to_gen = names_to_gen (* @ [eq_name]*) in - let gen_tac x = - NTactics.generalize_tac - ~where:("",0,(Some (mk_id x),[], Some NotationPt.UserInput)) in - let gen_eq = NTactics.generalize_tac - ~where:("",0,(Some (mk_appl [mk_id "jmeq_to_eq"; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne; - mk_id eq_name]),[], Some NotationPt.UserInput)) in - NTactics.block_tac ((List.map gen_tac names_to_gen)@gen_eq:: - [NTactics.clear_tac names_to_gen; - NTactics.try_tac (NTactics.clear_tac [eq_name]); - NTactics.apply_tac ("",0, mk_appl [streicher_id; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne]); - NTactics.reduce_tac ~reduction:(`Normalize true) - ~where:default_pattern] @ - (let names_to_intro = List.rev names_to_gen in - List.map NTactics.intro_tac names_to_intro)) status - | _ -> assert false + let streicher_id = mk_id "streicherK" in + let names_to_gen, _ = + cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in + let gen_tac x = generalize0_tac (List.map mk_id x) in + + match s with + (* jmeq *) + | NCic.Appl [_;_;_;_;_] -> + let names_to_gen = List.rev names_to_gen in + (*let gen_eq = NTactics.generalize_tac + ~where:("",0,(Some (mk_appl [mk_id "jmeq_to_eq"; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + mk_id eq_name]),[], Some + NotationPt.UserInput)) in*) + let gen_eq = generalize0_tac + [mk_appl [mk_id "jmeq_to_eq"; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + mk_id eq_name]] in + NTactics.block_tac ((gen_tac (List.rev names_to_gen))::gen_eq:: + [NTactics.clear_tac names_to_gen; + NTactics.try_tac (NTactics.clear_tac [eq_name]); + NTactics.apply_tac ("",0, mk_appl [streicher_id; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne]); + ] @ + (List.map NTactics.intro_tac names_to_gen)) status + + (* leibniz *) + | NCic.Appl [_;_;_;_] -> + begin + let names_to_gen, _ = + cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in + let names_to_gen = eq_name :: (List.rev names_to_gen) in + NTactics.block_tac ((gen_tac names_to_gen):: + [NTactics.clear_tac names_to_gen; + NTactics.apply_tac ("",0, mk_appl [streicher_id; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne]) + (* NTactics.reduce_tac ~reduction:(`Normalize true) + ~where:default_pattern *) + ] @ + let names_to_intro = List.tl names_to_gen in + (List.map NTactics.intro_tac names_to_intro)) status + end + | _ -> assert false + ;; let get_ctx st goal = @@ -514,20 +579,21 @@ let get_ctx st goal = (* = select + classify *) let select_eq ctx acc domain status goal = - let classify ~subst ctx' l r = + let classify ~use_jmeq ~subst ctx' l r = (* FIXME: metasenv *) if NCicReduction.are_convertible status ~metasenv:[] ~subst ctx' l r then status, `Identity - else status, (match hd_of_term l, hd_of_term r with + else status, (match hd_of_term status (mk_cic_term ctx' l), + hd_of_term status (mk_cic_term ctx' r) with | NCic.Const (NReference.Ref (_,NReference.Con (_,ki,nleft)) as kref), NCic.Const (NReference.Ref (_,NReference.Con (_,kj,_))) -> - if ki != kj then `Discriminate (0,true) + if ki != kj then `Discriminate (0,true, use_jmeq) else let rit = NReference.mk_indty true kref in let _,_,its,_,itno = NCicEnvironment.get_checked_indtys status rit in let it = List.nth its itno in let newprods = nargs it nleft (ki-1) in - `Discriminate (newprods, false) + `Discriminate (newprods, false, use_jmeq) | NCic.Rel j, _ when NCicTypeChecker.does_not_occur status ~subst ctx' (j-1) j r && l = NCic.Rel j -> `Subst `LeftToRight @@ -549,12 +615,12 @@ let select_eq ctx acc domain status goal = let status, kind = match ty with | NCic.Appl [NCic.Const (NReference.Ref (u,_)) ;_;l;r] when NUri.name_of_uri u = "eq" -> - classify ~subst:(get_subst status) ctx_ty l r + classify ~use_jmeq:false ~subst:(get_subst status) ctx_ty l r | NCic.Appl [NCic.Const (NReference.Ref (u,_)) ;lty;l;rty;r] when NUri.name_of_uri u = "jmeq" && NCicReduction.are_convertible status ~metasenv:[] ~subst:(get_subst status) ctx_ty lty rty - -> classify ~subst:(get_subst status) ctx_ty l r + -> classify ~use_jmeq:true ~subst:(get_subst status) ctx_ty l r | _ -> status, `NonEq in match kind with | `Identity -> @@ -570,7 +636,43 @@ let select_eq ctx acc domain status goal = in aux 0 ;; -let rec destruct_tac0 nprods acc domain skip status goal = +let tagged_intro_tac curtag name = + match curtag with + | _ -> NTactics.intro_tac name +(* | `Eq use_jmeq -> + 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) ] *) + +(* status in + distribute_tac (fun s g -> + let eq_name,(NCic.Decl s | NCic.Def (s,_)) = List.nth context (cur_eq-1) in + let _,ctx' = HExtlib.split_nth cur_eq context in + let status, s = NTacStatus.whd status ctx' (mk_cic_term ctx' s) in + let status, s = term_of_cic_term status s ctx' in + let use_jmeq = + match s with + | NCic.Appl [_;it;t1;t2] -> false + | NCic.Appl [_;it;t1;_;t2] -> true + | _ -> assert false in + ) status + let it, t1, t2, use_jmeq = match s with + | NCic.Appl [_;it;t1;t2] -> it,t1,t2,false + | NCic.Appl [_;it;t1;_;t2] -> it,t1,t2,true + | _ -> assert false in + [ NTactics.intro_tac name + ; NTactics.reduce_tac ~reduction:(`Whd true) ~where:prod_pattern ]*) +;; + +let rec destruct_tac0 tags acc domain skip status goal = + let pptag = function + | `Eq false -> "eq" + | `Eq true -> "jmeq" + | `Notag -> "reg" + in + let pptags tags = String.concat ", " (List.map pptag tags) in let ctx = get_ctx status goal in let subst = get_subst status in let get_newgoal os ns ogoal = @@ -582,25 +684,33 @@ let rec destruct_tac0 nprods acc domain skip status goal = pp (lazy ("destruct: acc is " ^ String.concat "," acc )); match selection, kind with | None, _ -> - pp (lazy (Printf.sprintf "destruct: nprods is %d, no selection, context is %s" nprods (status#ppcontext ~metasenv:[] ~subst ctx))); - if nprods > 0 then + pp (lazy (Printf.sprintf + "destruct: no selection, context is %s, stack is %s" + (status#ppcontext ~metasenv:[] ~subst ctx) (pptags tags))); + (match tags with + | [] -> status + | curtag::tags' -> let fresh = mk_fresh_name ctx 'e' 0 in - let status' = NTactics.exec (NTactics.intro_tac fresh) status goal in - destruct_tac0 (nprods-1) acc (fresh::domain) skip status' (get_newgoal status status' goal) - else - status - | Some cur_eq, `Discriminate (newprods,conflict) -> - pp (lazy (Printf.sprintf "destruct: discriminate - nprods is %d, selection is %d, context is %s" nprods cur_eq (status#ppcontext ~metasenv:[] ~subst ctx))); + let status' = NTactics.exec (tagged_intro_tac curtag fresh) status goal in + destruct_tac0 tags' acc (fresh::domain) skip status' + (get_newgoal status status' goal)) + | Some cur_eq, `Discriminate (newprods,conflict,use_jmeq) -> + pp (lazy (Printf.sprintf + "destruct: discriminate - nselection is %d, context is %s,stack is %s" + cur_eq (status#ppcontext ~metasenv:[] ~subst ctx) (pptags tags))); let status' = NTactics.exec (discriminate_tac ~context:ctx cur_eq) status goal in if conflict then status' else - destruct_tac0 (nprods+newprods) + let newtags = HExtlib.mk_list (`Eq use_jmeq) newprods in + destruct_tac0 (newtags@tags) (name_of_rel ~context:ctx cur_eq::acc) (List.filter (fun x -> x <> name_of_rel ~context:ctx cur_eq) domain) skip status' (get_newgoal status status' goal) | Some cur_eq, `Subst dir -> - pp (lazy (Printf.sprintf "destruct: subst - nprods is %d, selection is %d, context is %s" nprods cur_eq (status#ppcontext ~metasenv:[] ~subst ctx))); + pp (lazy (Printf.sprintf + "destruct: subst - selection is %d, context is %s, stack is %s" + cur_eq (status#ppcontext ~metasenv:[] ~subst ctx) (pptags tags))); let status' = NTactics.exec (subst_tac ~context:ctx ~dir skip cur_eq) status goal in pp (lazy (Printf.sprintf " ctx after subst = %s" (status#ppcontext ~metasenv:[] ~subst (get_ctx status' (get_newgoal status status' goal))))); let eq_name,_ = List.nth ctx (cur_eq-1) in @@ -613,9 +723,11 @@ let rec destruct_tac0 nprods acc domain skip status goal = let acc = rm_eq has_cleared acc in let skip = rm_eq has_cleared skip in let domain = rm_eq has_cleared domain in - destruct_tac0 nprods acc domain skip status' newgoal + destruct_tac0 tags acc domain skip status' newgoal | Some cur_eq, `Identity -> - pp (lazy (Printf.sprintf "destruct: identity - nprods is %d, selection is %d, context is %s" nprods cur_eq (status#ppcontext ~metasenv:[] ~subst ctx))); + pp (lazy (Printf.sprintf + "destruct: identity - selection is %d, context is %s, stack is %s" + cur_eq (status#ppcontext ~metasenv:[] ~subst ctx) (pptags tags))); let eq_name,_ = List.nth ctx (cur_eq-1) in let status' = NTactics.exec (clearid_tac ~context:ctx skip cur_eq) status goal in let newgoal = get_newgoal status status' goal in @@ -627,12 +739,16 @@ let rec destruct_tac0 nprods acc domain skip status goal = let acc = rm_eq has_cleared acc in let skip = rm_eq has_cleared skip in let domain = rm_eq has_cleared domain in - destruct_tac0 nprods acc domain skip status' newgoal + destruct_tac0 tags acc domain skip status' newgoal | Some cur_eq, `Cycle -> (* TODO, should never happen *) - pp (lazy (Printf.sprintf "destruct: cycle - nprods is %d, selection is %d, context is %s" nprods cur_eq (status#ppcontext ~metasenv:[] ~subst ctx))); + pp (lazy (Printf.sprintf + "destruct: cycle - selection is %d, context is %s, stack is %s" + cur_eq (status#ppcontext ~metasenv:[] ~subst ctx) (pptags tags))); assert false | Some cur_eq, `Blob -> - pp (lazy (Printf.sprintf "destruct: blob - nprods is %d, selection is %d, context is %s" nprods cur_eq (status#ppcontext ~metasenv:[] ~subst ctx))); + pp (lazy (Printf.sprintf + "destruct: blob - selection is %d, context is %s, stack is %s" + cur_eq (status#ppcontext ~metasenv:[] ~subst ctx) (pptags tags))); assert false | _ -> assert false ;; @@ -645,4 +761,4 @@ let destruct_tac dom skip s = | None -> List.map (fun (n,_) -> n) ctx | Some l -> l in - destruct_tac0 0 [] domain skip s' g) s;; + destruct_tac0 [] [] domain skip s' g) s;; diff --git a/matitaB/components/ng_tactics/nDestructTac.mli b/matitaB/components/ng_tactics/nDestructTac.mli index 714638d24..f753fa61e 100644 --- a/matitaB/components/ng_tactics/nDestructTac.mli +++ b/matitaB/components/ng_tactics/nDestructTac.mli @@ -13,3 +13,9 @@ val destruct_tac : string list option -> string list -> 's NTacStatus.tactic +val mk_discriminator: (use_jmeq: bool) -> + string -> NCic.inductiveType -> int -> + (#NTacStatus.tac_status as 's) -> string -> 's * NCic.obj + +exception ConstructorTooBig of string + diff --git a/matitaB/components/ng_tactics/nTactics.mli b/matitaB/components/ng_tactics/nTactics.mli index 985849b63..5290a322e 100644 --- a/matitaB/components/ng_tactics/nTactics.mli +++ b/matitaB/components/ng_tactics/nTactics.mli @@ -54,6 +54,7 @@ val rewrite_tac: dir:[ `LeftToRight | `RightToLeft ] -> what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic +val generalize0_tac : NotationPt.term list -> 's NTacStatus.tactic val generalize_tac : where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic val clear_tac : string list -> 's NTacStatus.tactic val reduce_tac: diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index 23bf4d396..30c138385 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -564,109 +564,122 @@ function callServer(servicename,processResponse,reqbody) } -function advanceForm1() -{ - processor = function(xml) { - if (is_defined(xml)) { - var parsed = xml.getElementsByTagName("parsed")[0]; - var ambiguity = xml.getElementsByTagName("ambiguity")[0]; - var disamberr = xml.getElementsByTagName("disamberror")[0]; - if (is_defined(parsed)) { - // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND"); - var len = parseInt(parsed.getAttribute("length")); - // len0 = unlocked.innerHTML.length; - var unescaped = unlocked.innerHTML.html_to_matita(); - var parsedtxt = parsed.childNodes[0].wholeText; - //parsedtxt = unescaped.substr(0,len); - var unparsedtxt = unescaped.substr(len); - lockedbackup += parsedtxt; - locked.innerHTML = lockedbackup; - unlocked.innerHTML = unparsedtxt.matita_to_html(); - // len1 = unlocked.innerHTML.length; - // len2 = len0 - len1; - var len2 = parsedtxt.length; - var metasenv = xml.getElementsByTagName("meta"); - populate_goalarray(metasenv); - init_autotraces(); - statements = listcons(len2,statements); - unlocked.scrollIntoView(true); - } - else if (is_defined(ambiguity)) { - var start = parseInt(ambiguity.getAttribute("start")); - var stop = parseInt(ambiguity.getAttribute("stop")); - var choices = xml.getElementsByTagName("choice"); - - matita.ambiguityStart = start; - matita.ambiguityStop = stop; - matita.unlockedbackup = unlocked.innerHTML.html_to_matita(); - matita.interpretations = []; - - var unlockedtxt = unlocked.innerHTML.html_to_matita(); - var pre = unlockedtxt.substring(0,start).matita_to_html(); - var mid = unlockedtxt.substring(start,stop).matita_to_html(); - var post = unlockedtxt.substring(stop).matita_to_html(); - unlocked.innerHTML = pre + - "" + - mid + "" + post; - - var title = "

Ambiguous input

"; - disambcell.innerHTML = title; - for (i = 0;i < choices.length;i++) { - matita.interpretations[i] = new Object(); +function advOneStep(xml) { + var parsed = xml.getElementsByTagName("parsed")[0]; + var ambiguity = xml.getElementsByTagName("ambiguity")[0]; + var disamberr = xml.getElementsByTagName("disamberror")[0]; + if (is_defined(parsed)) { + // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND"); + var len = parseInt(parsed.getAttribute("length")); + // len0 = unlocked.innerHTML.length; + var unescaped = unlocked.innerHTML.html_to_matita(); + var parsedtxt = parsed.childNodes[0].wholeText; + //parsedtxt = unescaped.substr(0,len); + var unparsedtxt = unescaped.substr(len); + lockedbackup += parsedtxt; + locked.innerHTML = lockedbackup; + unlocked.innerHTML = unparsedtxt.matita_to_html(); + // len1 = unlocked.innerHTML.length; + // len2 = len0 - len1; + var len2 = parsedtxt.length; + var metasenv = xml.getElementsByTagName("meta"); + statements = listcons(len2,statements); + unlocked.scrollIntoView(true); + return len; + } + else if (is_defined(ambiguity)) { + var start = parseInt(ambiguity.getAttribute("start")); + var stop = parseInt(ambiguity.getAttribute("stop")); + var choices = xml.getElementsByTagName("choice"); + + matita.ambiguityStart = start; + matita.ambiguityStop = stop; + matita.unlockedbackup = unlocked.innerHTML.html_to_matita(); + matita.interpretations = []; + + var unlockedtxt = unlocked.innerHTML.html_to_matita(); + var pre = unlockedtxt.substring(0,start).matita_to_html(); + var mid = unlockedtxt.substring(start,stop).matita_to_html(); + var post = unlockedtxt.substring(stop).matita_to_html(); + unlocked.innerHTML = pre + + "" + + mid + "" + post; + + var title = "

Ambiguous input

"; + disambcell.innerHTML = title; + for (i = 0;i < choices.length;i++) { + matita.interpretations[i] = new Object(); + + var href = choices[i].getAttribute("href"); + var title = choices[i].getAttribute("title"); + var desc = choices[i].childNodes[0].nodeValue; + + matita.interpretations[i].href = href; + matita.interpretations[i].title = title; + matita.interpretations[i].desc = desc; + + var choice = document.createElement("input"); + choice.setAttribute("type","radio"); + choice.setAttribute("name","interpr"); + choice.setAttribute("href",href); + choice.setAttribute("title",title); + if (i == 0) choice.setAttribute("checked",""); + + disambcell.appendChild(choice); + disambcell.appendChild(document.createTextNode(desc)); + disambcell.appendChild(document.createElement("br")); + } - var href = choices[i].getAttribute("href"); - var title = choices[i].getAttribute("title"); - var desc = choices[i].childNodes[0].nodeValue; + var okbutton = document.createElement("input"); + okbutton.setAttribute("type","button"); + okbutton.setAttribute("value","OK"); + okbutton.setAttribute("onclick","do_disambiguate()"); + var cancelbutton = document.createElement("input"); + cancelbutton.setAttribute("type","button"); + cancelbutton.setAttribute("value","Cancel"); + cancelbutton.setAttribute("onclick","cancel_disambiguate()"); - matita.interpretations[i].href = href; - matita.interpretations[i].title = title; - matita.interpretations[i].desc = desc; - - var choice = document.createElement("input"); - choice.setAttribute("type","radio"); - choice.setAttribute("name","interpr"); - choice.setAttribute("href",href); - choice.setAttribute("title",title); - if (i == 0) choice.setAttribute("checked",""); - - disambcell.appendChild(choice); - disambcell.appendChild(document.createTextNode(desc)); - disambcell.appendChild(document.createElement("br")); - } + disambcell.appendChild(okbutton); + disambcell.appendChild(cancelbutton); - var okbutton = document.createElement("input"); - okbutton.setAttribute("type","button"); - okbutton.setAttribute("value","OK"); - okbutton.setAttribute("onclick","do_disambiguate()"); - var cancelbutton = document.createElement("input"); - cancelbutton.setAttribute("type","button"); - cancelbutton.setAttribute("value","Cancel"); - cancelbutton.setAttribute("onclick","cancel_disambiguate()"); + disable_toparea(); - disambcell.appendChild(okbutton); - disambcell.appendChild(cancelbutton); + matita.disambMode = true; + updateSide(); + throw "Stop"; + } + else if (is_defined(disamberr)) { + set_cps(disamberr.childNodes); + matita.unlockedbackup = unlocked.innerHTML.html_to_matita(); + matita.disambMode = true; + disable_toparea(); + next_cp(0); + throw "Stop"; + } + else { + var error = xml.getElementsByTagName("error")[0]; + unlocked.innerHTML = error.childNodes[0].wholeText; + // debug(xml.childNodes[0].nodeValue); + throw "Stop"; + } - disable_toparea(); +} - matita.disambMode = true; - updateSide(); - } - else if (is_defined(disamberr)) { - set_cps(disamberr.childNodes); - matita.unlockedbackup = unlocked.innerHTML.html_to_matita(); - matita.disambMode = true; - disable_toparea(); - next_cp(0); - } - else { - var error = xml.getElementsByTagName("error")[0]; - unlocked.innerHTML = error.childNodes[0].wholeText; - // debug(xml.childNodes[0].nodeValue); - } +function advanceForm1() +{ + processor = function(xml) { + try { + if (is_defined(xml)) { + advOneStep(xml); + populate_goalarray(metasenv); + init_autotraces(); } else { debug("advance failed"); } - resume(); + } catch (e) { + // nothing to do + }; + resume(); }; pause(); callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape()); @@ -984,6 +997,7 @@ function gotoTop() callServer("top",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape()); } + function gotoPos(offset) { if (!is_defined(offset)) { @@ -991,6 +1005,8 @@ function gotoPos(offset) } processor = function(xml) { if (is_defined(xml)) { + try { + /* parsed = xml.getElementsByTagName("parsed")[0]; len = parseInt(parsed.getAttribute("length")); // len0 = unlocked.innerHTML.length; @@ -1008,6 +1024,8 @@ function gotoPos(offset) statements = listcons(len2,statements); unlocked.scrollIntoView(true); // la populate non andrebbe fatta a ogni passo + */ + var len = advOneStep(xml); if (offset <= len) { init_autotraces(); populate_goalarray(metasenv); @@ -1015,6 +1033,11 @@ function gotoPos(offset) } else { gotoPos(offset - len); } + } catch (er) { + init_autotraces(); + populate_goalarray(metasenv); + resume(); + } } else { init_autotraces(); unlocked.scrollIntoView(true); -- 2.39.2