From 30743ffb0d331aaaa449957238128943ba781ecf Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Wed, 22 Apr 2009 10:43:52 +0000 Subject: [PATCH] New command "inverter" used to generate an induction/inversion principle for inductive types. The syntax is: inverter name_of_the_principle for name_of_inductive_type param_selection where param_selection is of the form (# # # ... #) where # can be either ? or %. The length of param_selection must match the number of right parameters of the inverted inductive_type. A % means that the corresponding parameter will have an inversion hypothesis, while a ? means that the parameter won't have an inversion hypothesis. Therefore, a selection (??...?) will generate the traditional elimination principle, while (%%...%) will generate a full inversion principle. Induction/inversion principles are useful for treating inductive types such that some of their right parameters are used uniformly in one or more constructors. If the inverted parameters are used uniformly in some constructor, the induction/inversion principle will provide an induction hypothesis for that branch (while a full inversion, also ranging on non-uniform parameters, would no provide a useful induction hypothesis). --- .../software/components/grafite/grafiteAst.ml | 3 +- .../components/grafite/grafiteAstPp.ml | 2 + .../grafite_engine/grafiteEngine.ml | 9 + .../grafite_parser/grafiteDisambiguate.ml | 5 + .../grafite_parser/grafiteParser.ml | 368 +++++++++--------- helm/software/components/tactics/.depend | 18 +- helm/software/components/tactics/inversion.ml | 67 ++-- .../software/components/tactics/inversion.mli | 2 +- .../components/tactics/inversion_principle.ml | 178 +++++---- .../tactics/inversion_principle.mli | 3 + .../components/urimanager/uriManager.ml | 20 + .../components/urimanager/uriManager.mli | 2 + 12 files changed, 385 insertions(+), 292 deletions(-) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 01053ca13..67d42c644 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -167,7 +167,7 @@ type ('term,'lazy_term) macro = (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 18 +let magic = 19 type ('term,'obj) command = | Index of loc * 'term option (* key *) * UriManager.uri (* value *) @@ -176,6 +176,7 @@ type ('term,'obj) command = | Coercion of loc * 'term * bool (* add_obj *) * int (* arity *) * int (* saturations *) | PreferCoercion of loc * 'term + | Inverter of loc * string * 'term * bool list | UnificationHint of loc * 'term * int (* term, precedence *) | Default of loc * string * UriManager.uri list | Drop of loc diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 4e10cfa8b..0fddb2163 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -332,6 +332,8 @@ let pp_command ~term_pp ~obj_pp = function pp_coercion ~term_pp t do_composites i j | PreferCoercion (_,t) -> "prefer coercion " ^ term_pp t + | Inverter (_,n,ty,params) -> + "inverter " ^ n ^ " for " ^ term_pp ty ^ " " ^ List.fold_left (fun acc x -> acc ^ (match x with true -> "%" | _ -> "?")) "" params | UnificationHint (_,t, n) -> "unification hint " ^ string_of_int n ^ " " ^ term_pp t | Default (_,what,uris) -> pp_default what uris diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index c06750039..2e8b49f7d 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -669,6 +669,15 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status eval_prefer_coercion status coercion | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) -> eval_coercion status ~add_composites uri arity saturations + | GrafiteAst.Inverter (loc, name, indty, params) -> + let buri = GrafiteTypes.get_baseuri status in + let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in + let indty_uri = + try CicUtil.uri_of_term indty + with Invalid_argument _ -> + raise (Invalid_argument "not an inductive type to invert") + in + Inversion_principle.build_inverter ~add_obj status uri indty_uri params | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n | GrafiteAst.Default (loc, what, uris) as cmd -> diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 76d553379..835e6b411 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -768,6 +768,11 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)= disambiguate_term None text prefix_len lexicon_status_ref [] in let metasenv,t = disambiguate_term metasenv t in !lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s) + | GrafiteAst.Inverter (loc,n,indty,params) -> + let lexicon_status_ref = ref lexicon_status in + let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref [] in + let metasenv,indty = disambiguate_term metasenv indty in + !lexicon_status_ref, metasenv, GrafiteAst.Inverter (loc,n,indty,params) | GrafiteAst.UnificationHint (loc, t, n) -> let lexicon_status_ref = ref lexicon_status in let disambiguate_term = diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 21051e12d..ff1771b5a 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -162,6 +162,20 @@ EXTEND None -> None,[],Some Ast.UserInput | Some ps -> ps] ]; + inverter_param_list: [ + [ params = tactic_term -> + let deannotate = function + | Ast.AttributedTerm (_,t) | t -> t + in match deannotate params with + | Ast.Implicit -> [false] + | Ast.UserInput -> [true] + | Ast.Appl l -> + List.map (fun x -> match deannotate x with + | Ast.Implicit -> false + | Ast.UserInput -> true + | _ -> raise (Invalid_argument "malformed target parameter list 1")) l + | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ] + ]; direction: [ [ SYMBOL ">" -> `LeftToRight | SYMBOL "<" -> `RightToLeft ] @@ -267,8 +281,8 @@ EXTEND let pattern = match pattern with | None -> None, [], Some Ast.UserInput | Some pattern -> pattern - in - GrafiteAst.Elim (loc, what, using, pattern, ispecs) + in + GrafiteAst.Elim (loc, what, using, pattern, ispecs) | IDENT "elimType"; what = tactic_term; using = using; (num, idents) = intros_spec -> GrafiteAst.ElimType (loc, what, using, (num, idents)) @@ -283,7 +297,7 @@ EXTEND raise (HExtlib.Localized (loc, CicNotationParser.Parse_error ("the pattern cannot specify the term to replace, only its" ^ " paths in the hypotheses and in the conclusion"))) - else + else GrafiteAst.Fold (loc, kind, t, p) | IDENT "fourier" -> GrafiteAst.Fourier loc @@ -480,8 +494,8 @@ EXTEND | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac) | LPAREN; tac = SELF; RPAREN -> tac | tac = tactic -> tac - ] - ]; + ] + ]; punctuation_tactical: [ [ SYMBOL "[" -> GrafiteAst.Branch loc @@ -499,7 +513,7 @@ EXTEND | IDENT "unfocus" -> GrafiteAst.Unfocus loc | IDENT "skip" -> GrafiteAst.Skip loc ] - ]; + ]; ntheorem_flavour: [ [ [ IDENT "ntheorem" ] -> `Theorem ] @@ -524,178 +538,178 @@ EXTEND SYMBOL ":"; fst_typ = term; SYMBOL <:unicode>; OPT SYMBOL "|"; fst_constructors = LIST0 constructor SEP SYMBOL "|"; tl = OPT [ "with"; - types = LIST1 [ - name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode>; - OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" -> - (name, true, typ, constructors) ] SEP "with" -> types - ] -> - let params = - List.fold_right - (fun (names, typ) acc -> - (List.map (fun name -> (name, typ)) names) @ acc) - params [] - in - let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in - let tl_ind_types = match tl with None -> [] | Some types -> types in - let ind_types = fst_ind_type :: tl_ind_types in - (params, ind_types) - ] ]; - - record_spec: [ [ - name = IDENT; - params = LIST0 protected_binder_vars; - SYMBOL ":"; typ = term; SYMBOL <:unicode>; SYMBOL "{" ; - fields = LIST0 [ - name = IDENT ; - coercion = [ - SYMBOL ":" -> false,0 - | SYMBOL ":"; SYMBOL ">" -> true,0 - | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity - ]; - ty = term -> - let b,n = coercion in - (name,ty,b,n) - ] SEP SYMBOL ";"; SYMBOL "}" -> - let params = - List.fold_right - (fun (names, typ) acc -> - (List.map (fun name -> (name, typ)) names) @ acc) - params [] - in - (params,name,typ,fields) - ] ]; - - macro: [ - [ [ IDENT "check" ]; t = term -> - GrafiteAst.Check (loc, t) - | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term -> - GrafiteAst.Eval (loc, kind, t) - | [ IDENT "inline"]; - style = OPT [ IDENT "procedural"; depth = OPT int -> depth ]; - suri = QSTRING; prefix = OPT QSTRING; - flavour = OPT [ "as"; attr = inline_flavour -> attr ] -> - let style = match style with - | None -> GrafiteAst.Declarative - | Some depth -> GrafiteAst.Procedural depth - in - let prefix = match prefix with None -> "" | Some prefix -> prefix in - GrafiteAst.Inline (loc,style,suri,prefix, flavour) - | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") -> - if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true) - | IDENT "auto"; params = auto_params -> - GrafiteAst.AutoInteractive (loc,params) - | [ IDENT "whelp"; "match" ] ; t = term -> - GrafiteAst.WMatch (loc,t) - | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> - GrafiteAst.WInstance (loc,t) - | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING -> - GrafiteAst.WLocate (loc,id) - | [ IDENT "whelp"; IDENT "elim" ] ; t = term -> - GrafiteAst.WElim (loc, t) - | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> - GrafiteAst.WHint (loc,t) - ] - ]; - alias_spec: [ - [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING -> - let alpha = "[a-zA-Z]" in - let num = "[0-9]+" in - let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in - let decoration = "\\'" in - let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in - let rex = Str.regexp ("^"^ident^"$") in - if Str.string_match rex id 0 then - if (try ignore (UriManager.uri_of_string uri); true - with UriManager.IllFormedUri _ -> false) - then - LexiconAst.Ident_alias (id, uri) - else - raise - (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri))) - else - raise (HExtlib.Localized (loc, CicNotationParser.Parse_error ( - Printf.sprintf "Not a valid identifier: %s" id))) - | IDENT "symbol"; symbol = QSTRING; - instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ]; - SYMBOL "="; dsc = QSTRING -> - let instance = - match instance with Some i -> i | None -> 0 + types = LIST1 [ + name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode>; + OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" -> + (name, true, typ, constructors) ] SEP "with" -> types + ] -> + let params = + List.fold_right + (fun (names, typ) acc -> + (List.map (fun name -> (name, typ)) names) @ acc) + params [] in - LexiconAst.Symbol_alias (symbol, instance, dsc) - | IDENT "num"; - instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ]; - SYMBOL "="; dsc = QSTRING -> - let instance = - match instance with Some i -> i | None -> 0 + let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in + let tl_ind_types = match tl with None -> [] | Some types -> types in + let ind_types = fst_ind_type :: tl_ind_types in + (params, ind_types) + ] ]; + + record_spec: [ [ + name = IDENT; + params = LIST0 protected_binder_vars; + SYMBOL ":"; typ = term; SYMBOL <:unicode>; SYMBOL "{" ; + fields = LIST0 [ + name = IDENT ; + coercion = [ + SYMBOL ":" -> false,0 + | SYMBOL ":"; SYMBOL ">" -> true,0 + | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity + ]; + ty = term -> + let b,n = coercion in + (name,ty,b,n) + ] SEP SYMBOL ";"; SYMBOL "}" -> + let params = + List.fold_right + (fun (names, typ) acc -> + (List.map (fun name -> (name, typ)) names) @ acc) + params [] in - LexiconAst.Number_alias (instance, dsc) - ] - ]; - argument: [ - [ l = LIST0 [ SYMBOL <:unicode> (* η *); SYMBOL "." -> () ]; - id = IDENT -> - Ast.IdentArg (List.length l, id) - ] - ]; - associativity: [ - [ IDENT "left"; IDENT "associative" -> Gramext.LeftA - | IDENT "right"; IDENT "associative" -> Gramext.RightA - | IDENT "non"; IDENT "associative" -> Gramext.NonA - ] - ]; - precedence: [ - [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ] - ]; - notation: [ - [ dir = OPT direction; s = QSTRING; - assoc = OPT associativity; prec = precedence; - IDENT "for"; - p2 = - [ blob = UNPARSED_AST -> - add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob) - (CicNotationParser.parse_level2_ast - (Ulexing.from_utf8_string blob)) - | blob = UNPARSED_META -> - add_raw_attribute ~text:(Printf.sprintf "${%s}" blob) - (CicNotationParser.parse_level2_meta - (Ulexing.from_utf8_string blob)) - ] -> - let assoc = - match assoc with - | None -> default_associativity - | Some assoc -> assoc + (params,name,typ,fields) + ] ]; + + macro: [ + [ [ IDENT "check" ]; t = term -> + GrafiteAst.Check (loc, t) + | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term -> + GrafiteAst.Eval (loc, kind, t) + | [ IDENT "inline"]; + style = OPT [ IDENT "procedural"; depth = OPT int -> depth ]; + suri = QSTRING; prefix = OPT QSTRING; + flavour = OPT [ "as"; attr = inline_flavour -> attr ] -> + let style = match style with + | None -> GrafiteAst.Declarative + | Some depth -> GrafiteAst.Procedural depth + in + let prefix = match prefix with None -> "" | Some prefix -> prefix in + GrafiteAst.Inline (loc,style,suri,prefix, flavour) + | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") -> + if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true) + | IDENT "auto"; params = auto_params -> + GrafiteAst.AutoInteractive (loc,params) + | [ IDENT "whelp"; "match" ] ; t = term -> + GrafiteAst.WMatch (loc,t) + | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> + GrafiteAst.WInstance (loc,t) + | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING -> + GrafiteAst.WLocate (loc,id) + | [ IDENT "whelp"; IDENT "elim" ] ; t = term -> + GrafiteAst.WElim (loc, t) + | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> + GrafiteAst.WHint (loc,t) + ] + ]; + alias_spec: [ + [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING -> + let alpha = "[a-zA-Z]" in + let num = "[0-9]+" in + let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in + let decoration = "\\'" in + let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in + let rex = Str.regexp ("^"^ident^"$") in + if Str.string_match rex id 0 then + if (try ignore (UriManager.uri_of_string uri); true + with UriManager.IllFormedUri _ -> false) + then + LexiconAst.Ident_alias (id, uri) + else + raise + (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri))) + else + raise (HExtlib.Localized (loc, CicNotationParser.Parse_error ( + Printf.sprintf "Not a valid identifier: %s" id))) + | IDENT "symbol"; symbol = QSTRING; + instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ]; + SYMBOL "="; dsc = QSTRING -> + let instance = + match instance with Some i -> i | None -> 0 in - let p1 = - add_raw_attribute ~text:s - (CicNotationParser.parse_level1_pattern prec - (Ulexing.from_utf8_string s)) + LexiconAst.Symbol_alias (symbol, instance, dsc) + | IDENT "num"; + instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ]; + SYMBOL "="; dsc = QSTRING -> + let instance = + match instance with Some i -> i | None -> 0 in - (dir, p1, assoc, prec, p2) - ] - ]; - level3_term: [ - [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u) - | id = IDENT -> Ast.VarPattern id - | SYMBOL "_" -> Ast.ImplicitPattern - | LPAREN; terms = LIST1 SELF; RPAREN -> - (match terms with - | [] -> assert false - | [term] -> term - | terms -> Ast.ApplPattern terms) - ] - ]; - interpretation: [ - [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term -> - (s, args, t) - ] - ]; - - include_command: [ [ - IDENT "include" ; path = QSTRING -> - loc,path,LexiconAst.WithPreferences - | IDENT "include'" ; path = QSTRING -> - loc,path,LexiconAst.WithoutPreferences - ]]; + LexiconAst.Number_alias (instance, dsc) + ] + ]; + argument: [ + [ l = LIST0 [ SYMBOL <:unicode> (* η *); SYMBOL "." -> () ]; + id = IDENT -> + Ast.IdentArg (List.length l, id) + ] + ]; + associativity: [ + [ IDENT "left"; IDENT "associative" -> Gramext.LeftA + | IDENT "right"; IDENT "associative" -> Gramext.RightA + | IDENT "non"; IDENT "associative" -> Gramext.NonA + ] + ]; + precedence: [ + [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ] + ]; + notation: [ + [ dir = OPT direction; s = QSTRING; + assoc = OPT associativity; prec = precedence; + IDENT "for"; + p2 = + [ blob = UNPARSED_AST -> + add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob) + (CicNotationParser.parse_level2_ast + (Ulexing.from_utf8_string blob)) + | blob = UNPARSED_META -> + add_raw_attribute ~text:(Printf.sprintf "${%s}" blob) + (CicNotationParser.parse_level2_meta + (Ulexing.from_utf8_string blob)) + ] -> + let assoc = + match assoc with + | None -> default_associativity + | Some assoc -> assoc + in + let p1 = + add_raw_attribute ~text:s + (CicNotationParser.parse_level1_pattern prec + (Ulexing.from_utf8_string s)) + in + (dir, p1, assoc, prec, p2) + ] + ]; + level3_term: [ + [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u) + | id = IDENT -> Ast.VarPattern id + | SYMBOL "_" -> Ast.ImplicitPattern + | LPAREN; terms = LIST1 SELF; RPAREN -> + (match terms with + | [] -> assert false + | [term] -> term + | terms -> Ast.ApplPattern terms) + ] + ]; + interpretation: [ + [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term -> + (s, args, t) + ] + ]; + + include_command: [ [ + IDENT "include" ; path = QSTRING -> + loc,path,LexiconAst.WithPreferences + | IDENT "include'" ; path = QSTRING -> + loc,path,LexiconAst.WithoutPreferences + ]]; grafite_command: [ [ IDENT "set"; n = QSTRING; v = QSTRING -> @@ -749,7 +763,11 @@ EXTEND GrafiteAst.Pump(loc,steps) | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term -> GrafiteAst.UnificationHint (loc, t, n) - | IDENT "record" ; (params,name,ty,fields) = record_spec -> + | IDENT "inverter"; name = IDENT; IDENT "for"; + indty = tactic_term; paramspec = inverter_param_list -> + GrafiteAst.Inverter + (loc, name, indty, paramspec) + | IDENT "record" ; (params,name,ty,fields) = record_spec -> GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields)) | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> let uris = List.map UriManager.uri_of_string uris in diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend index e7aa8868d..29482257c 100644 --- a/helm/software/components/tactics/.depend +++ b/helm/software/components/tactics/.depend @@ -1,19 +1,11 @@ -proofEngineTypes.cmi: proofEngineHelpers.cmi: proofEngineTypes.cmi -proofEngineReduction.cmi: continuationals.cmi: proofEngineTypes.cmi tacticals.cmi: proofEngineTypes.cmi reductionTactics.cmi: proofEngineTypes.cmi proofEngineStructuralRules.cmi: proofEngineTypes.cmi primitiveTactics.cmi: proofEngineTypes.cmi -hashtbl_equiv.cmi: metadataQuery.cmi: proofEngineTypes.cmi -universe.cmi: autoTypes.cmi: proofEngineTypes.cmi -autoCache.cmi: -paramodulation/utils.cmi: -closeCoercionGraph.cmi: -paramodulation/subst.cmi: paramodulation/equality.cmi: paramodulation/utils.cmi \ paramodulation/subst.cmi paramodulation/founif.cmi: paramodulation/subst.cmi @@ -24,7 +16,8 @@ paramodulation/indexing.cmi: paramodulation/utils.cmi \ paramodulation/equality.cmi paramodulation/saturation.cmi: paramodulation/utils.cmi proofEngineTypes.cmi \ paramodulation/indexing.cmi paramodulation/equality.cmi -automationCache.cmi: universe.cmi paramodulation/saturation.cmi +automationCache.cmi: universe.cmi paramodulation/saturation.cmi \ + paramodulation/equality.cmi variousTactics.cmi: proofEngineTypes.cmi compose.cmi: proofEngineTypes.cmi introductionTactics.cmi: proofEngineTypes.cmi @@ -34,13 +27,10 @@ equalityTactics.cmi: proofEngineTypes.cmi auto.cmi: proofEngineTypes.cmi automationCache.cmi destructTactic.cmi: proofEngineTypes.cmi inversion.cmi: proofEngineTypes.cmi -inversion_principle.cmi: ring.cmi: proofEngineTypes.cmi setoids.cmi: proofEngineTypes.cmi -fourier.cmi: fourierR.cmi: proofEngineTypes.cmi fwdSimplTactic.cmi: proofEngineTypes.cmi -history.cmi: statefulProofEngine.cmi: proofEngineTypes.cmi tactics.cmi: tacticals.cmi proofEngineTypes.cmi automationCache.cmi auto.cmi declarative.cmi: proofEngineTypes.cmi automationCache.cmi auto.cmi @@ -119,9 +109,9 @@ paramodulation/saturation.cmx: paramodulation/utils.cmx \ paramodulation/indexing.cmx paramodulation/founif.cmx \ paramodulation/equality.cmx paramodulation/saturation.cmi automationCache.cmo: universe.cmi paramodulation/saturation.cmi \ - automationCache.cmi + paramodulation/equality.cmi automationCache.cmi automationCache.cmx: universe.cmx paramodulation/saturation.cmx \ - automationCache.cmi + paramodulation/equality.cmx automationCache.cmi variousTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ variousTactics.cmi variousTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ diff --git a/helm/software/components/tactics/inversion.ml b/helm/software/components/tactics/inversion.ml index 3b4000ea4..13b350daf 100644 --- a/helm/software/components/tactics/inversion.ml +++ b/helm/software/components/tactics/inversion.ml @@ -28,7 +28,7 @@ exception TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple exception NotAnInductiveTypeToEliminate -let debug = false;; +let debug = true;; let debug_print = fun msg -> if debug then prerr_endline (Lazy.force msg) else () @@ -49,22 +49,25 @@ let rec baseuri_of_term = function | _ -> raise (Invalid_argument "baseuri_of_term") (* returns DX1 = DX1 -> ... DXn=DXn -> GOALTY *) -let rec foo_cut nleft parameters parameters_ty body uri_of_eq = +let rec foo_cut nleft parameters parameters_ty body uri_of_eq selections = if nleft > 0 then foo_cut (nleft-1) (List.tl parameters) (List.tl parameters_ty) body - uri_of_eq + uri_of_eq selections else - match parameters with - | hd::tl -> + match parameters,selections with + | hd::tl, x::xs when x -> Cic.Prod ( Cic.Anonymous, Cic.Appl[Cic.MutInd (uri_of_eq ,0,[]); (List.hd parameters_ty) ; hd; hd], foo_cut nleft (List.map (CicSubstitution.lift 1) tl) (List.map (CicSubstitution.lift 1) (List.tl parameters_ty)) - (CicSubstitution.lift 1 body) uri_of_eq ) - | [] -> body + (CicSubstitution.lift 1 body) uri_of_eq xs) + | hd::tl,x::xs -> + foo_cut nleft tl (List.tl parameters_ty) body uri_of_eq xs + | [],[] -> body + | _ -> raise (Invalid_argument "inverter: the selection doesn't match the arity of the specified inductive type") ;; (* from a complex Cic.Prod term, return the list of its components *) @@ -106,10 +109,15 @@ let foo_appl nleft nright_consno term uri = ;; +(* induction/inversion, abbastanza semplicemente, consiste nel generare i prod + * delle uguaglianze corrispondenti ai soli parametri destri appartenenti all'insieme S. + * Attenzione al caso base: cos'e` replace_lifting? + * S = {} e` il principio di induzione + * S = insieme_dei_destri e` il principio di inversione *) let rec foo_prod nright right_param_tys rightparameters l2 base_rel goalty - uri_of_eq rightparameters_ termty isSetType term = - match right_param_tys with - | hd::tl -> Cic.Prod ( + uri_of_eq rightparameters_ termty isSetType term selections selections_ = + match right_param_tys, selections with + | hd::tl, x::xs when x -> Cic.Prod ( Cic.Anonymous, Cic.Appl [Cic.MutInd(uri_of_eq,0,[]); hd; (List.hd rightparameters); @@ -121,21 +129,32 @@ let rec foo_prod nright right_param_tys rightparameters l2 base_rel goalty base_rel (CicSubstitution.lift 1 goalty) uri_of_eq (List.map (CicSubstitution.lift 1) rightparameters_) (CicSubstitution.lift 1 termty) - isSetType (CicSubstitution.lift 1 term)) - | [] -> ProofEngineReduction.replace_lifting + isSetType (CicSubstitution.lift 1 term)) xs selections_ + | hd::tl, x::xs -> + foo_prod (nright-1) tl (List.tl rightparameters) l2 + (base_rel-1) goalty uri_of_eq rightparameters_ termty + isSetType term xs selections_ + | [],[] -> + ProofEngineReduction.replace_lifting ~equality:(fun _ -> CicUtil.alpha_equivalence) ~context:[] ~what: (if isSetType - then (rightparameters_ @ [term] ) - else (rightparameters_ ) ) + then rightparameters_ @ [term] + else rightparameters_ ) ~with_what: (List.map (CicSubstitution.lift (-1)) l2) ~where:goalty + | _ -> raise (Invalid_argument "inverter: the selection doesn't match the arity of the specified inductive type") (* the same subterm of goalty could be simultaneously sx and dx!*) ;; +(* induction/inversion, abbastanza semplicemente, consiste nel generare i lambda + * soltanto per i parametri destri appartenenti all'insieme S. + * Warning: non ne sono piu` cosi` sicuro... + * S = {} e` il principio di induzione + * S = insieme_dei_destri e` il principio di inversione *) let rec foo_lambda nright right_param_tys nright_ right_param_tys_ rightparameters created_vars base_rel goalty uri_of_eq rightparameters_ - termty isSetType term = + termty isSetType term selections = match right_param_tys with | hd::tl -> Cic.Lambda ( (Cic.Name ("lambda" ^ (string_of_int nright))), @@ -148,7 +167,7 @@ let rec foo_lambda nright right_param_tys nright_ right_param_tys_ base_rel (CicSubstitution.lift 1 goalty) uri_of_eq (List.map (CicSubstitution.lift 1) rightparameters_) (CicSubstitution.lift 1 termty) isSetType - (CicSubstitution.lift 1 term)) + (CicSubstitution.lift 1 term)) selections | [] when isSetType -> Cic.Lambda ( (Cic.Name ("lambda" ^ (string_of_int nright))), (ProofEngineReduction.replace_lifting @@ -163,10 +182,10 @@ let rec foo_lambda nright right_param_tys nright_ right_param_tys_ (base_rel+1) (CicSubstitution.lift 1 goalty) uri_of_eq (List.map (CicSubstitution.lift 1) rightparameters_) (CicSubstitution.lift 1 termty) isSetType - (CicSubstitution.lift 1 term)) + (CicSubstitution.lift 1 term)) selections selections | [] -> foo_prod nright_ right_param_tys_ rightparameters created_vars - base_rel goalty uri_of_eq rightparameters_ - termty isSetType term + base_rel goalty uri_of_eq rightparameters_ + termty isSetType term selections selections ;; let isSetType paramty = ((Pervasives.compare @@ -174,7 +193,7 @@ let isSetType paramty = ((Pervasives.compare (Cic.Sort Cic.Prop)) != 0) exception EqualityNotDefinedYet -let private_inversion_tac ~term = +let private_inversion_tac ~term selections = let module T = CicTypeChecker in let module R = CicReduction in let module C = Cic in @@ -223,7 +242,7 @@ let private_inversion_tac ~term = let nright= ((List.length parameters)- nleft) in let isSetType = isSetType paramty in let cut_term = foo_cut nleft parameters - parameters_tys goalty uri_of_eq in + parameters_tys goalty uri_of_eq selections in (*DEBUG*) debug_print (lazy ("cut term " ^ CicPp.ppterm cut_term)); debug_print (lazy ("CONTEXT before apply HCUT: " ^ (CicMetaSubst.ppcontext ~metasenv [] context ))); @@ -242,14 +261,16 @@ let private_inversion_tac ~term = (* apply (ledx_ind( lambda x. lambda y, ...)) *) let t1,metasenv,_subst,t3,t4, attrs = proof2 in let goal2 = List.hd (List.tl gl1) in - let (_,context,_) = CicUtil.lookup_meta goal2 metasenv in + let (_,context,g2ty) = CicUtil.lookup_meta goal2 metasenv in (* rightparameters type list *) let rightparam_ty_l = (cut_first nleft parameters_tys) in (* rightparameters list *) let rightparameters= cut_first nleft parameters in + debug_print + (lazy ("Right param: " ^ (CicPp.ppterm (Cic.Appl rightparameters)))); let lambda_t = foo_lambda nright rightparam_ty_l nright rightparam_ty_l rightparameters [] nright goalty uri_of_eq rightparameters termty isSetType - term in + term selections in let t = foo_appl nleft (nright+consno) lambda_t eliminator_uri in debug_print (lazy ("Lambda_t: " ^ (CicPp.ppterm t))); debug_print (lazy ("Term: " ^ (CicPp.ppterm termty))); diff --git a/helm/software/components/tactics/inversion.mli b/helm/software/components/tactics/inversion.mli index 2c8b996ff..46cf97ed9 100644 --- a/helm/software/components/tactics/inversion.mli +++ b/helm/software/components/tactics/inversion.mli @@ -25,5 +25,5 @@ val isSetType: Cic.term -> bool exception EqualityNotDefinedYet (* raised by private_inversion_tac only *) -val private_inversion_tac: term: Cic.term -> ProofEngineTypes.tactic +val private_inversion_tac: term: Cic.term -> bool list -> ProofEngineTypes.tactic val inversion_tac: term: Cic.term -> ProofEngineTypes.tactic diff --git a/helm/software/components/tactics/inversion_principle.ml b/helm/software/components/tactics/inversion_principle.ml index ae0a48186..e15e8cb63 100644 --- a/helm/software/components/tactics/inversion_principle.ml +++ b/helm/software/components/tactics/inversion_principle.ml @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -let debug = false;; +let debug = true;; let debug_print = fun msg -> if debug then prerr_endline (Lazy.force msg) else () @@ -129,93 +129,116 @@ let rec build_theorem rightparam_tys arity_l (*arity_l only to name p's*) [(Cic.Rel 1)] uri typeno ) ;; +let build_one typeno inversor_uri indty_uri nleft arity cons_list selections = + (*check if there are right parameters, else return void*) + if List.length (list_of_prod arity) = (nleft + 1) then + None + else + try + let arity_l = cut_last (list_of_prod arity) in + let rightparam_tys = cut_first nleft arity_l in + let theorem = build_theorem rightparam_tys arity_l arity cons_list + [](*created_vars*) [](*created_vars_ty*) nleft indty_uri typeno in + debug_print + (lazy ("theorem prima di refine: " ^ (CicPp.ppterm theorem))); + let (ref_theorem,_,metasenv,_) = + CicRefine.type_of_aux' [] [] theorem CicUniv.oblivion_ugraph in + (*DEBUG*) debug_print + (lazy ("theorem dopo refine: " ^ (CicPp.ppterm ref_theorem))); + let goal = CicMkImplicit.new_meta metasenv [] in + let metasenv' = (goal,[],ref_theorem)::metasenv in + let attrs = [`Class (`InversionPrinciple); `Generated] in + let _subst = [] in + let proof= + Some inversor_uri,metasenv',_subst, + lazy (Cic.Meta(goal,[])),ref_theorem, attrs in + let _,applies = + List.fold_right + (fun _ (i,applies) -> + i+1,PrimitiveTactics.apply_tac (Cic.Rel i)::applies + ) cons_list (2,[]) in + let proof1,gl1 = + ProofEngineTypes.apply_tactic + (Tacticals.then_ + ~start:(PrimitiveTactics.intros_tac ()) + (*if the number of applies is 1, we cannot use + thens, but then_*) + ~continuation: + (match List.length applies with + 0 -> Inversion.private_inversion_tac (Cic.Rel 1) selections + | 1 -> + Tacticals.then_ + ~start:(Inversion.private_inversion_tac (Cic.Rel 1) selections) + ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2)) + | _ -> + Tacticals.thens + ~start:(Inversion.private_inversion_tac (Cic.Rel 1) selections) + ~continuations:applies)) + (proof,goal) in + let _,metasenv,_subst,bo,ty, attrs = proof1 in + assert (metasenv = []); + Some + (inversor_uri, + Cic.Constant + (UriManager.name_of_uri inversor_uri,Some (Lazy.force bo),ty,[],[])) + with + Inversion.EqualityNotDefinedYet -> + HLog.warn "No default equality, no inversion principle"; + None + | CicRefine.RefineFailure ls -> + HLog.warn + ("CicRefine.RefineFailure during generation of inversion principle: " ^ + Lazy.force ls) ; + None + | CicRefine.Uncertain ls -> + HLog.warn + ("CicRefine.Uncertain during generation of inversion principle: " ^ + Lazy.force ls) ; + None + | CicRefine.AssertFailure ls -> + HLog.warn + ("CicRefine.AssertFailure during generation of inversion principle: " ^ + Lazy.force ls) ; + None +;; + +let build_inverter ~add_obj status u indty_uri params = + let indty_uri, indty_no, _ = UriManager.ind_uri_split indty_uri in + let indty_no = match indty_no with None -> raise (Invalid_argument "not an inductive type")| Some n -> n in + let indty, univ = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph indty_uri + in + match indty with + | Cic.InductiveDefinition (tys,_,nleft,attrs) -> + let _,inductive,_,_ = List.hd tys in + if not inductive then raise (Invalid_argument "not an inductive type") + else + let name,_,arity,cons_list = List.nth tys (indty_no-1) in + (match build_one (indty_no-1) u indty_uri nleft arity cons_list params with + | None -> status,[] + | Some (uri, obj) -> + let status, added = add_obj uri obj status in + status, uri::added) + | _ -> assert false +;; + let build_inversion ~add_obj ~add_coercion uri obj = match obj with | Cic.InductiveDefinition (tys,_,nleft,attrs) -> let _,inductive,_,_ = List.hd tys in if not inductive then [] else - let build_one typeno name nleft arity cons_list = - (*check if there are right parameters, else return void*) - if List.length (list_of_prod arity) = (nleft + 1) then - None - else - try - let arity_l = cut_last (list_of_prod arity) in - let rightparam_tys = cut_first nleft arity_l in - let theorem = build_theorem rightparam_tys arity_l arity cons_list - [](*created_vars*) [](*created_vars_ty*) nleft uri typeno in - debug_print - (lazy ("theorem prima di refine: " ^ (CicPp.ppterm theorem))); - let (ref_theorem,_,metasenv,_) = - CicRefine.type_of_aux' [] [] theorem CicUniv.oblivion_ugraph in - (*DEBUG*) debug_print - (lazy ("theorem dopo refine: " ^ (CicPp.ppterm ref_theorem))); - let buri = UriManager.buri_of_uri uri in - let inversor_uri = - UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in - let goal = CicMkImplicit.new_meta metasenv [] in - let metasenv' = (goal,[],ref_theorem)::metasenv in - let attrs = [`Class (`InversionPrinciple); `Generated] in - let _subst = [] in - let proof= - Some inversor_uri,metasenv',_subst, - lazy (Cic.Meta(goal,[])),ref_theorem, attrs in - let _,applies = - List.fold_right - (fun _ (i,applies) -> - i+1,PrimitiveTactics.apply_tac (Cic.Rel i)::applies - ) cons_list (2,[]) in - let proof1,gl1 = - ProofEngineTypes.apply_tactic - (Tacticals.then_ - ~start:(PrimitiveTactics.intros_tac ()) - (*if the number of applies is 1, we cannot use - thens, but then_*) - ~continuation: - (match List.length applies with - 0 -> Inversion.private_inversion_tac (Cic.Rel 1) - | 1 -> - Tacticals.then_ - ~start:(Inversion.private_inversion_tac (Cic.Rel 1)) - ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2)) - | _ -> - Tacticals.thens - ~start:(Inversion.private_inversion_tac (Cic.Rel 1)) - ~continuations:applies)) - (proof,goal) in - let _,metasenv,_subst,bo,ty, attrs = proof1 in - assert (metasenv = []); - Some - (inversor_uri, - Cic.Constant - (UriManager.name_of_uri inversor_uri,Some (Lazy.force bo),ty,[],[])) - with - Inversion.EqualityNotDefinedYet -> - HLog.warn "No default equality, no inversion principle"; - None - | CicRefine.RefineFailure ls -> - HLog.warn - ("CicRefine.RefineFailure during generation of inversion principle: " ^ - Lazy.force ls) ; - None - | CicRefine.Uncertain ls -> - HLog.warn - ("CicRefine.Uncertain during generation of inversion principle: " ^ - Lazy.force ls) ; - None - | CicRefine.AssertFailure ls -> - HLog.warn - ("CicRefine.AssertFailure during generation of inversion principle: " ^ - Lazy.force ls) ; - None - in let counter = ref (List.length tys) in let all_inverters = List.fold_right (fun (name,_,arity,cons_list) res -> + let arity_l = cut_last (list_of_prod arity) in + let rightparam_tys = cut_first nleft arity_l in + let params = HExtlib.mk_list true (List.length rightparam_tys) in + let buri = UriManager.buri_of_uri uri in + let inversor_uri = + UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in counter := !counter-1; - match build_one !counter name nleft arity cons_list with + match build_one !counter inversor_uri uri nleft arity cons_list params with None -> res | Some inv -> inv::res ) tys [] @@ -226,6 +249,5 @@ let build_inversion ~add_obj ~add_coercion uri obj = | _ -> [] ;; - let init () = LibrarySync.add_object_declaration_hook build_inversion;; diff --git a/helm/software/components/tactics/inversion_principle.mli b/helm/software/components/tactics/inversion_principle.mli index 30335ed6c..5ceec20a4 100644 --- a/helm/software/components/tactics/inversion_principle.mli +++ b/helm/software/components/tactics/inversion_principle.mli @@ -25,3 +25,6 @@ (* $Id: primitiveTactics.ml 9014 2008-09-26 08:03:47Z tassi $ *) val init: unit -> unit +val build_inverter: add_obj:(UriManager.uri -> Cic.obj -> 'b -> 'b * UriManager.uri list) -> + 'b -> UriManager.uri -> UriManager.uri -> bool list -> + 'b * UriManager.uri list diff --git a/helm/software/components/urimanager/uriManager.ml b/helm/software/components/urimanager/uriManager.ml index c0da8eb4b..9107994a1 100644 --- a/helm/software/components/urimanager/uriManager.ml +++ b/helm/software/components/urimanager/uriManager.ml @@ -191,6 +191,26 @@ let bodyuri_of_uri (uri, _) = None ;; +let ind_uri_split ((s, _) as uri) = + let noxp = strip_xpointer uri in + let length = String.length s in + try + (let arg_index = String.rindex s '(' in + try + (let ty_index = String.index_from s arg_index '/' in + try + (let k_index = String.index_from s (ty_index+1) '/' in + let tyno = int_of_string (String.sub s (ty_index + 1) (k_index - ty_index - 1)) in + let kno = int_of_string (String.sub s (k_index + 1) (String.length s - k_index - 2)) in + noxp, Some tyno, Some kno) + with Not_found -> + let tyno = int_of_string (String.sub s (ty_index + 1) (String.length s - ty_index - 2)) in + noxp, Some tyno, None) + with Not_found -> noxp, None, None + ) + with Not_found -> noxp, None, None +;; + (* these are bugged! * we should remove _types, _univ, _ann all toghether *) let innertypesuri_of_uri (uri, _) = diff --git a/helm/software/components/urimanager/uriManager.mli b/helm/software/components/urimanager/uriManager.mli index 0d4fcb419..99e65ab88 100644 --- a/helm/software/components/urimanager/uriManager.mli +++ b/helm/software/components/urimanager/uriManager.mli @@ -56,6 +56,8 @@ val uri_is_ind : uri -> bool (* it gives back None if the uri refers to a Variable or MutualInductiveType *) val bodyuri_of_uri : uri -> uri option +val ind_uri_split : uri -> uri * int option * int option + (* given an uri, it gives back the uri of its inner types *) val innertypesuri_of_uri : uri -> uri (* given an uri, it gives back the uri of its univgraph *) -- 2.39.2