From 0575a1cb077087970f311b48f2e45dc4a01a6867 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 27 Apr 2005 17:01:49 +0000 Subject: [PATCH] merged changes from the svn fork by me and Enrico --- .../cic_disambiguation/cicTextualLexer2.ml | 7 +- .../cic_disambiguation/cicTextualParser2.ml | 324 +++++++------- .../cic_disambiguation/cicTextualParser2.mli | 6 +- helm/ocaml/cic_disambiguation/disambiguate.ml | 22 +- .../ocaml/cic_disambiguation/disambiguate.mli | 30 +- helm/ocaml/cic_disambiguation/test_parser.ml | 19 +- helm/ocaml/cic_omdoc/doubleTypeInference.ml | 6 +- helm/ocaml/cic_proof_checking/.depend | 18 +- helm/ocaml/cic_proof_checking/Makefile | 9 - .../cic_proof_checking/cicEnvironment.mli | 2 +- ...cicReductionMachine.ml => cicReduction.ml} | 2 +- .../cicReductionMachine.mli | 33 -- .../cic_proof_checking/cicReductionNaif.ml | 407 ------------------ .../cic_proof_checking/cicReductionNaif.mli | 35 -- .../cic_proof_checking/cicSubstitution.ml | 4 +- .../cic_proof_checking/cicSubstitution.mli | 6 +- .../cic_proof_checking/cicTypeChecker.ml | 12 +- helm/ocaml/cic_transformations/tacticAst.ml | 143 +++--- .../cic_transformations/tacticAst2Box.ml | 151 ++++--- helm/ocaml/cic_transformations/tacticAstPp.ml | 175 ++++---- .../ocaml/cic_transformations/tacticAstPp.mli | 6 +- helm/ocaml/cic_unification/cicMetaSubst.ml | 6 +- helm/ocaml/cic_unification/cicRefine.ml | 14 +- helm/ocaml/cic_unification/cicUnification.ml | 18 +- helm/ocaml/cic_unification/coercGraph.ml | 4 +- helm/ocaml/cic_unification/coercGraph.mli | 2 + helm/ocaml/hbugs/Makefile | 2 +- helm/ocaml/hbugs/broker.ml | 1 - helm/ocaml/hbugs/hbugs_common.ml | 22 +- helm/ocaml/hbugs/hbugs_messages.ml | 44 +- helm/ocaml/hbugs/hbugs_types.mli | 22 +- .../ocaml/hbugs/search_pattern_apply_tutor.ml | 2 +- helm/ocaml/tactics/tacticals.ml | 10 +- helm/ocaml/tactics/tacticals.mli | 4 +- helm/ocaml/tactics/tactics.ml | 1 + helm/ocaml/tactics/tactics.mli | 1 + helm/ocaml/tactics/variousTactics.ml | 8 + helm/ocaml/tactics/variousTactics.mli | 3 + helm/ocaml/urimanager/uriManager.ml | 16 + helm/ocaml/urimanager/uriManager.mli | 3 + 40 files changed, 610 insertions(+), 990 deletions(-) rename helm/ocaml/cic_proof_checking/{cicReductionMachine.ml => cicReduction.ml} (99%) delete mode 100644 helm/ocaml/cic_proof_checking/cicReductionMachine.mli delete mode 100644 helm/ocaml/cic_proof_checking/cicReductionNaif.ml delete mode 100644 helm/ocaml/cic_proof_checking/cicReductionNaif.mli diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml index 6f179505d..650b69723 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml @@ -106,6 +106,9 @@ let rec token' = lexer and token = lexer *) + +let remove_quotes s = String.sub s 1 (String.length s - 2) + let rec token comments = lexer | blanks -> token comments lexbuf | uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf) @@ -119,9 +122,7 @@ let rec token comments = lexer | meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf) | implicit -> return lexbuf ("IMPLICIT", Ulexing.utf8_lexeme lexbuf) | qstring -> - let lexeme = Ulexing.utf8_lexeme lexbuf in - let s = String.sub lexeme 1 (String.length lexeme - 2) in - return lexbuf ("QSTRING", s) + return lexbuf ("QSTRING", remove_quotes (Ulexing.utf8_lexeme lexbuf)) | symbol -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf) | tex_token -> let macro = diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index d32302a13..d7096ae79 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -65,12 +65,12 @@ let tactic = Grammar.Entry.create grammar "tactic" let tactical = Grammar.Entry.create grammar "tactical" let tactical0 = Grammar.Entry.create grammar "tactical0" let command = Grammar.Entry.create grammar "command" +let alias_spec = Grammar.Entry.create grammar "alias_spec" +let macro = Grammar.Entry.create grammar "macro" let script = Grammar.Entry.create grammar "script" +let statement = Grammar.Entry.create grammar "statement" let return_term loc term = CicAst.AttributedTerm (`Loc loc, term) -let return_tactic loc tactic = TacticAst.LocatedTactic (loc, tactic) -let return_tactical loc tactical = TacticAst.LocatedTactical (loc, tactical) -let return_command loc cmd = cmd (* TODO ZACK FIXME uhm ... why we drop loc? *) let fail floc msg = let (x, y) = CicAst.loc_of_floc floc in @@ -88,6 +88,12 @@ let int_opt = function | None -> None | Some lexeme -> Some (int_of_string lexeme) +let int_of_string s = + try + Pervasives.int_of_string s + with Failure _ -> + failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s) + (** the uri of an inductive type (a ".ind" uri) is not meaningful without an * xpointer. Still, it's likely that an user who wrote "cic:/blabla/foo.ind" * actually meant "cic:/blabla/foo.ind#xpointer(1/1)", i.e. the first inductive @@ -110,7 +116,7 @@ let mk_binder_ast binder typ vars body = vars body EXTEND - GLOBAL: term term0 tactic tactical tactical0 command script; + GLOBAL: term term0 statement; int: [ [ num = NUM -> try @@ -318,132 +324,126 @@ EXTEND [ PAREN "["; idents = LIST1 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ] ]; reduction_kind: [ - [ [ IDENT "reduce" | IDENT "Reduce" ] -> `Reduce - | [ IDENT "simplify" | IDENT "Simplify" ] -> `Simpl - | [ IDENT "whd" | IDENT "Whd" ] -> `Whd ] + [ [ IDENT "reduce" ] -> `Reduce + | [ IDENT "simplify" ] -> `Simpl + | [ IDENT "whd" ] -> `Whd ] ]; tactic: [ - [ [ IDENT "absurd" | IDENT "Absurd" ]; t = tactic_term -> - return_tactic loc (TacticAst.Absurd t) - | [ IDENT "apply" | IDENT "Apply" ]; t = tactic_term -> - return_tactic loc (TacticAst.Apply t) - | [ IDENT "assumption" | IDENT "Assumption" ] -> - return_tactic loc TacticAst.Assumption - | [ IDENT "auto" | IDENT "Auto" ] -> return_tactic loc TacticAst.Auto - | [ IDENT "change" | IDENT "Change" ]; + [ [ IDENT "absurd" ]; t = tactic_term -> + TacticAst.Absurd (loc, t) + | [ IDENT "apply" ]; t = tactic_term -> + TacticAst.Apply (loc, t) + | [ IDENT "assumption" ] -> + TacticAst.Assumption loc + | [ IDENT "auto" ] -> TacticAst.Auto loc + | [ IDENT "change" ]; t1 = tactic_term; "with"; t2 = tactic_term; where = tactic_where -> - return_tactic loc (TacticAst.Change (t1, t2, where)) + TacticAst.Change (loc, t1, t2, where) (* TODO Change_pattern *) - | [ IDENT "contradiction" | IDENT "Contradiction" ] -> - return_tactic loc TacticAst.Contradiction - | [ IDENT "cut" | IDENT "Cut" ]; - t = tactic_term -> return_tactic loc (TacticAst.Cut t) - | [ IDENT "decompose" | IDENT "Decompose" ]; + | [ IDENT "contradiction" ] -> + TacticAst.Contradiction loc + | [ IDENT "cut" ]; + t = tactic_term -> + TacticAst.Cut (loc, t) + | [ IDENT "decompose" ]; principles = ident_list1; where = IDENT -> - return_tactic loc (TacticAst.Decompose (where, principles)) - | [ IDENT "discriminate" | IDENT "Discriminate" ]; + TacticAst.Decompose (loc, where, principles) + | [ IDENT "discriminate" ]; hyp = IDENT -> - return_tactic loc (TacticAst.Discriminate hyp) - | [ IDENT "elimType" | IDENT "ElimType" ]; t = tactic_term -> - return_tactic loc (TacticAst.ElimType t) - | [ IDENT "elim" | IDENT "Elim" ]; + TacticAst.Discriminate (loc, hyp) + | [ IDENT "elimType" ]; t = tactic_term -> + TacticAst.ElimType (loc, t) + | [ IDENT "elim" ]; t1 = tactic_term; using = OPT [ "using"; using = tactic_term -> using ] -> - return_tactic loc (TacticAst.Elim (t1, using)) - | [ IDENT "exact" | IDENT "Exact" ]; t = tactic_term -> - return_tactic loc (TacticAst.Exact t) - | [ IDENT "exists" | IDENT "Exists" ] -> - return_tactic loc TacticAst.Exists - | [ IDENT "fold" | IDENT "Fold" ]; + TacticAst.Elim (loc, t1, using) + | [ IDENT "exact" ]; t = tactic_term -> + TacticAst.Exact (loc, t) + | [ IDENT "exists" ] -> + TacticAst.Exists loc + | [ IDENT "fold" ]; kind = reduction_kind; t = tactic_term -> - return_tactic loc (TacticAst.Fold (kind, t)) - | [ IDENT "fourier" | IDENT "Fourier" ] -> - return_tactic loc TacticAst.Fourier - | [ IDENT "hint" | IDENT "Hint" ] -> return_tactic loc TacticAst.Hint - | [ IDENT "injection" | IDENT "Injection" ]; ident = IDENT -> - return_tactic loc (TacticAst.Injection ident) - | [ IDENT "intros" | IDENT "Intros" ]; + TacticAst.Fold (loc, kind, t) + | [ IDENT "fourier" ] -> + TacticAst.Fourier loc + | IDENT "goal"; n = NUM -> TacticAst.Goal (loc, int_of_string n) + | [ IDENT "hint" ] -> TacticAst.Hint loc + | [ IDENT "injection" ]; ident = IDENT -> + TacticAst.Injection (loc, ident) + | [ IDENT "intros" ]; num = OPT [ num = int -> num ]; idents = OPT ident_list0 -> let idents = match idents with None -> [] | Some idents -> idents in - return_tactic loc (TacticAst.Intros (num, idents)) - | [ IDENT "intro" | IDENT "Intro" ] -> - return_tactic loc (TacticAst.Intros (None, [])) - | [ IDENT "left" | IDENT "Left" ] -> return_tactic loc TacticAst.Left + TacticAst.Intros (loc, num, idents) + | [ IDENT "intro" ] -> + TacticAst.Intros (loc, None, []) + | [ IDENT "left" ] -> TacticAst.Left loc | [ "let" | "Let" ]; t = tactic_term; "in"; where = IDENT -> - return_tactic loc (TacticAst.LetIn (t, where)) + TacticAst.LetIn (loc, t, where) | kind = reduction_kind; pat = OPT [ "in"; pat = [ IDENT "goal" -> `Goal | IDENT "hyp" -> `Everywhere ] -> pat ]; terms = LIST0 term SEP SYMBOL "," -> - let tac = - (match (pat, terms) with - | None, [] -> TacticAst.Reduce (kind, None) - | None, terms -> TacticAst.Reduce (kind, Some (terms, `Goal)) - | Some pat, [] -> TacticAst.Reduce (kind, Some ([], pat)) - | Some pat, terms -> TacticAst.Reduce (kind, Some (terms, pat))) - in - return_tactic loc tac - | [ IDENT "reflexivity" | IDENT "Reflexivity" ] -> - return_tactic loc TacticAst.Reflexivity - | [ IDENT "replace" | IDENT "Replace" ]; + (match (pat, terms) with + | None, [] -> TacticAst.Reduce (loc, kind, None) + | None, terms -> TacticAst.Reduce (loc, kind, Some (terms, `Goal)) + | Some pat, [] -> TacticAst.Reduce (loc, kind, Some ([], pat)) + | Some pat, terms -> TacticAst.Reduce (loc, kind, Some (terms, pat))) + | [ IDENT "reflexivity" ] -> + TacticAst.Reflexivity loc + | [ IDENT "replace" ]; t1 = tactic_term; "with"; t2 = tactic_term -> - return_tactic loc (TacticAst.Replace (t1, t2)) + TacticAst.Replace (loc, t1, t2) (* TODO Rewrite *) (* TODO Replace_pattern *) - | [ IDENT "right" | IDENT "Right" ] -> return_tactic loc TacticAst.Right - | [ IDENT "ring" | IDENT "Ring" ] -> return_tactic loc TacticAst.Ring - | [ IDENT "split" | IDENT "Split" ] -> return_tactic loc TacticAst.Split - | [ IDENT "symmetry" | IDENT "Symmetry" ] -> - return_tactic loc TacticAst.Symmetry - | [ IDENT "transitivity" | IDENT "Transitivity" ]; + | [ IDENT "right" ] -> TacticAst.Right loc + | [ IDENT "ring" ] -> TacticAst.Ring loc + | [ IDENT "split" ] -> TacticAst.Split loc + | [ IDENT "symmetry" ] -> + TacticAst.Symmetry loc + | [ IDENT "transitivity" ]; t = tactic_term -> - return_tactic loc (TacticAst.Transitivity t) + TacticAst.Transitivity (loc, t) ] ]; - tactical0: [ [ t = tactical; SYMBOL "." -> return_tactical loc t ] ]; tactical: - [ "command" NONA - [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ] - | "sequence" LEFTA - [ tactics = LIST1 NEXT SEP SYMBOL ";" -> - (match tactics with - | [tactic] -> tactic - | _ -> return_tactical loc (TacticAst.Seq tactics)) + [ "sequence" LEFTA + [ tacticals = LIST1 NEXT SEP SYMBOL ";" -> + TacticAst.Seq (loc, tacticals) ] | "then" NONA [ tac = tactical; PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" -> - return_tactical loc (TacticAst.Then (tac, tacs)) + (TacticAst.Then (loc, tac, tacs)) ] | "loops" RIGHTA - [ [ IDENT "do" | IDENT "Do" ]; count = int; tac = tactical -> - return_tactical loc (TacticAst.Do (count, tac)) - | [ IDENT "repeat" | IDENT "Repeat" ]; tac = tactical -> - return_tactical loc (TacticAst.Repeat tac) + [ [ IDENT "do" ]; count = int; tac = tactical -> + TacticAst.Do (loc, count, tac) + | [ IDENT "repeat" ]; tac = tactical -> + TacticAst.Repeat (loc, tac) ] | "simple" NONA - [ [ IDENT "tries" | IDENT "Tries" ]; + [ IDENT "tries"; PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" -> - return_tactical loc (TacticAst.Tries tacs) - | [ IDENT "try" | IDENT "Try" ]; tac = NEXT -> - return_tactical loc (TacticAst.Try tac) - | [ IDENT "fail" | IDENT "Fail" ] -> return_tactical loc TacticAst.Fail - | [ IDENT "id" | IDENT "Id" ] -> return_tactical loc TacticAst.IdTac - | PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac - | tac = tactic -> return_tactical loc (TacticAst.Tactic tac) + TacticAst.Tries (loc, tacs) + | IDENT "try"; tac = NEXT -> + TacticAst.Try (loc, tac) + | IDENT "fail" -> TacticAst.Fail loc + | IDENT "id" -> TacticAst.IdTac loc + | PAREN "("; tac = tactical; PAREN ")" -> tac + | tac = tactic -> TacticAst.Tactic (loc, tac) ] ]; - theorem_flavour: [ (* all flavours but Goal *) - [ [ IDENT "definition" | IDENT "Definition" ] -> `Definition - | [ IDENT "fact" | IDENT "Fact" ] -> `Fact - | [ IDENT "lemma" | IDENT "Lemma" ] -> `Lemma - | [ IDENT "remark" | IDENT "Remark" ] -> `Remark - | [ IDENT "theorem" | IDENT "Theorem" ] -> `Theorem + theorem_flavour: [ + [ [ IDENT "definition" ] -> `Definition + | [ IDENT "fact" ] -> `Fact + | [ IDENT "lemma" ] -> `Lemma + | [ IDENT "remark" ] -> `Remark + | [ IDENT "theorem" ] -> `Theorem ] ]; inductive_spec: [ [ @@ -469,27 +469,63 @@ EXTEND let ind_types = fst_ind_type :: tl_ind_types in (params, ind_types) ] ]; - print_kind: [ - [ [ IDENT "Env" | IDENT "env" | IDENT "Environment" | IDENT "environment" ] - -> `Env - | [ IDENT "Coer" | IDENT "coer" | IDENT "Coercions" | IDENT "coercions" ] - -> `Coer - ] ]; - command: [ - [ [ IDENT "abort" | IDENT "Abort" ] -> return_command loc TacticAst.Abort - | [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof - | [ IDENT "quit" | IDENT "Quit" ] -> return_command loc TacticAst.Quit - | [ IDENT "qed" | IDENT "Qed" ] -> - return_command loc (TacticAst.Qed None) - | [ IDENT "print" | IDENT "Print" ]; - print_kind = print_kind -> - return_command loc (TacticAst.Print print_kind) - | [ IDENT "save" | IDENT "Save" ]; name = IDENT -> - return_command loc (TacticAst.Qed (Some name)) + macro: [[ + [ IDENT "abort" ] -> TacticAst.Abort loc + | [ IDENT "quit" ] -> TacticAst.Quit loc + | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name) + | [ IDENT "undo" ]; steps = OPT NUM -> + TacticAst.Undo (loc, int_opt steps) + | [ IDENT "redo" ]; steps = OPT NUM -> + TacticAst.Redo (loc, int_opt steps) + | [ IDENT "check" ]; t = term -> + TacticAst.Check (loc, t) + | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name) + ]]; + + 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 ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in + let rex = Str.regexp ("^"^ident^"$") in + if Str.string_match rex id 0 then + let rex = Str.regexp + ("^\\(cic:/\\|theory:/\\)"^ident^ + "\\(/"^ident^"+\\)*\\(\\."^ident^"\\)+"^ + "\\(#xpointer("^ num^"\\(/"^num^"\\)+)\\)?$") + in + if Str.string_match rex uri 0 then + TacticAst.Ident_alias (id, uri) + else + raise (Parse_error (loc,sprintf "Not a valid uri: %s" uri)) + else + raise (Parse_error (loc,sprintf "Not a valid identifier: %s" id)) + | IDENT "symbol"; symbol = QSTRING; + instance = OPT [ PAREN "("; IDENT "instance"; n = NUM; PAREN ")" -> n ]; + SYMBOL "="; dsc = QSTRING -> + let instance = + match instance with Some i -> int_of_string i | None -> 0 + in + TacticAst.Symbol_alias (symbol, instance, dsc) + | IDENT "num"; + instance = OPT [ PAREN "("; IDENT "instance"; n = NUM; PAREN ")" -> n ]; + SYMBOL "="; dsc = QSTRING -> + let instance = + match instance with Some i -> int_of_string i | None -> 0 + in + TacticAst.Number_alias (instance, dsc) + ] + ]; + + command: [[ + [ IDENT "set" ]; n = QSTRING; v = QSTRING -> + TacticAst.Set (loc, n, v) + | [ IDENT "qed" ] -> TacticAst.Qed loc | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> - return_command loc (TacticAst.Theorem (flavour, name, typ, body)) + TacticAst.Theorem (loc, flavour, name, typ, body) | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; defs = let_defs -> let name,ty = @@ -500,48 +536,33 @@ EXTEND | _ -> assert false in let body = CicAst.Ident (name,None) in - TacticAst.Theorem(`Definition, Some name, ty, + TacticAst.Theorem(loc, `Definition, Some name, ty, Some (CicAst.LetRec (ind_kind, defs, body))) - | [ IDENT "inductive" | IDENT "Inductive" ]; spec = inductive_spec -> + | [ IDENT "inductive" ]; spec = inductive_spec -> let (params, ind_types) = spec in - return_command loc (TacticAst.Inductive (params, ind_types)) - | [ IDENT "coinductive" | IDENT "CoInductive" ]; spec = inductive_spec -> + TacticAst.Inductive (loc, params, ind_types) + | [ 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 - return_command loc (TacticAst.Inductive (params, ind_types)) - | [ IDENT "coercion" | IDENT "Coercion" ] ; name = IDENT -> - return_command loc (TacticAst.Coercion (CicAst.Ident (name,Some []))) - | [ IDENT "coercion" | IDENT "Coercion" ] ; name = URI -> - return_command loc (TacticAst.Coercion (CicAst.Uri (name,Some []))) - | [ IDENT "goal" | IDENT "Goal" ]; typ = term; - body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> - return_command loc (TacticAst.Theorem (`Goal, None, typ, body)) - | [ IDENT "undo" | IDENT "Undo" ]; steps = OPT NUM -> - return_command loc (TacticAst.Undo (int_opt steps)) - | [ IDENT "redo" | IDENT "Redo" ]; steps = OPT NUM -> - return_command loc (TacticAst.Redo (int_opt steps)) - | [ IDENT "baseuri" | IDENT "Baseuri" ]; uri = OPT QSTRING -> - return_command loc (TacticAst.Baseuri uri) - | [ IDENT "basedir" | IDENT "Basedir" ]; uri = OPT QSTRING -> - return_command loc (TacticAst.Basedir uri) - | [ IDENT "check" | IDENT "Check" ]; t = term -> - return_command loc (TacticAst.Check t) -(* - | [ IDENT "alias" | IDENT "Alias" ]; spec = alias_spec -> - return_command loc (TacticAst.Alias spec) -*) - ] - ]; - script_entry: [ - [ cmd = tactical0 -> Command cmd -(* | s = COMMENT -> Comment (loc, s) *) + TacticAst.Inductive (loc, params, ind_types) + | [ IDENT "coercion" ] ; name = IDENT -> + TacticAst.Coercion (loc, CicAst.Ident (name,Some [])) + | [ IDENT "coercion" ] ; name = URI -> + TacticAst.Coercion (loc, CicAst.Uri (name,Some [])) + | [ IDENT "alias" ]; spec = alias_spec -> + TacticAst.Alias (loc, spec) + ]]; + + statement: [ + [ cmd = command; SYMBOL "." -> TacticAst.Command (loc, cmd) + | tac = tactical; SYMBOL "." -> TacticAst.Tactical (loc, tac) + | mac = macro; SYMBOL "." -> TacticAst.Macro (loc, mac) ] ]; - script: [ [ entries = LIST0 script_entry; EOI -> (loc, entries) ] ]; END let exc_located_wrapper f = @@ -555,12 +576,8 @@ let exc_located_wrapper f = let parse_term stream = exc_located_wrapper (fun () -> (Grammar.Entry.parse term0 stream)) -let parse_tactic stream = - exc_located_wrapper (fun () -> (Grammar.Entry.parse tactic stream)) -let parse_tactical stream = - exc_located_wrapper (fun () -> (Grammar.Entry.parse tactical0 stream)) -let parse_script stream = - exc_located_wrapper (fun () -> (Grammar.Entry.parse script stream)) +let parse_statement stream = + exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream)) (**/**) @@ -581,12 +598,13 @@ module EnvironmentP3 = (fun domain_item (dsc, _) acc -> let s = match domain_item with - | Id id -> sprintf "alias id %s = %s" id dsc - | Symbol (symb, instance) -> - sprintf "alias symbol \"%s\" (instance %d) = \"%s\"" - symb instance dsc - | Num instance -> - sprintf "alias num (instance %d) = \"%s\"" instance dsc + | Id id -> + TacticAstPp.pp_alias (TacticAst.Ident_alias (id, dsc)) ^ "." + | Symbol (symb, i) -> + TacticAstPp.pp_alias (TacticAst.Symbol_alias (symb, i, dsc)) + ^ "." + | Num i -> + TacticAstPp.pp_alias (TacticAst.Number_alias (i, dsc)) ^ "." in s :: acc) env [] diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli index 659bb2aa5..f7510a9bd 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli @@ -27,10 +27,8 @@ exception Parse_error of Token.flocation * string (** {2 Parsing functions} *) -val parse_term: char Stream.t -> DisambiguateTypes.term -val parse_tactic: char Stream.t -> DisambiguateTypes.tactic -val parse_tactical: char Stream.t -> DisambiguateTypes.tactical -val parse_script: char Stream.t -> DisambiguateTypes.script +val parse_term: char Stream.t -> DisambiguateTypes.term +val parse_statement: char Stream.t -> (CicAst.term, string) TacticAst.statement (** {2 Grammar extensions} *) diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 54478c81a..552e3d30b 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -417,6 +417,21 @@ let domain_diff dom1 dom2 = in List.filter (fun elt -> not (is_in_dom2 elt)) dom1 +module type Disambiguator = +sig + val disambiguate_term : + dbd:Mysql.dbd -> + context:Cic.context -> + metasenv:Cic.metasenv -> + ?initial_ugraph:CicUniv.universe_graph -> + aliases:environment -> (* previous interpretation status *) + CicAst.term -> + (environment * (* new interpretation status *) + Cic.metasenv * (* new metasenv *) + Cic.term* + CicUniv.universe_graph) list (* disambiguated term *) +end + module Make (C: Callbacks) = struct let choices_of_id dbd id = @@ -449,8 +464,9 @@ module Make (C: Callbacks) = fun _ _ _ -> term)) uris - let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term + let disambiguate_term ~(dbd:Mysql.dbd) ~context ~metasenv ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env + term = debug_print "NEW DISAMBIGUATE INPUT"; let disambiguate_context = (* cic context -> disambiguate context *) @@ -625,8 +641,8 @@ struct ?(aliases=DisambiguateTypes.Environment.empty) term = let ast = CicTextualParser2.parse_term (Stream.of_string term) in try - Disambiguator.disambiguate_term ~dbd context metasenv ast ?initial_ugraph - ~aliases + Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast + ?initial_ugraph ~aliases with Exit -> raise (Ambiguous_term term) end diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index 3eff90ad6..ac9b97792 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -29,20 +29,22 @@ open DisambiguateTypes exception NoWellTypedInterpretation -module Make (C : Callbacks) : - sig - val disambiguate_term : - dbd:Mysql.dbd -> - Cic.context -> - Cic.metasenv -> - CicAst.term -> - ?initial_ugraph:CicUniv.universe_graph -> - aliases:environment -> (* previous interpretation status *) - (environment * (* new interpretation status *) - Cic.metasenv * (* new metasenv *) - Cic.term* - CicUniv.universe_graph) list (* disambiguated term *) - end +module type Disambiguator = +sig + val disambiguate_term : + dbd:Mysql.dbd -> + context:Cic.context -> + metasenv:Cic.metasenv -> + ?initial_ugraph:CicUniv.universe_graph -> + aliases:environment -> (* previous interpretation status *) + CicAst.term -> + (environment * (* new interpretation status *) + Cic.metasenv * (* new metasenv *) + Cic.term* + CicUniv.universe_graph) list (* disambiguated term *) +end + +module Make (C : Callbacks) : Disambiguator module Trivial: sig diff --git a/helm/ocaml/cic_disambiguation/test_parser.ml b/helm/ocaml/cic_disambiguation/test_parser.ml index 356c0a369..31bcdad05 100644 --- a/helm/ocaml/cic_disambiguation/test_parser.ml +++ b/helm/ocaml/cic_disambiguation/test_parser.ml @@ -30,17 +30,16 @@ let pp_tactical = TacticAst2Box.tacticalPp let mode = try match Sys.argv.(1) with - | "alias" -> prerr_endline "Alias"; `Alias | "term" -> prerr_endline "Term"; `Term - | "tactic" -> prerr_endline "Tactic"; `Tactic - | "tactical" | "command" -> prerr_endline "Tactical"; `Tactical - | "script" -> prerr_endline "Script"; `Script + | "statement" -> prerr_endline "Statement"; `Statement +(* | "script" -> prerr_endline "Script"; `Script *) | _ -> prerr_endline "What???????"; exit 1 with Invalid_argument _ -> prerr_endline "Term"; `Term let _ = +(* if mode = `Script then let ic = open_in Sys.argv.(2) in let istream = Stream.of_channel ic in @@ -51,6 +50,7 @@ let _ = | DisambiguateTypes.Comment (loc, s) -> print_endline s) script else +*) let ic = stdin in try while true do @@ -61,12 +61,17 @@ let _ = | `Term -> let term = CicTextualParser2.parse_term istream in print_endline (BoxPp.pp_term term) - | `Tactic -> - let tac = CicTextualParser2.parse_tactic istream in - print_endline (TacticAstPp.pp_tactic tac) + | `Statement -> + (match CicTextualParser2.parse_statement istream with + | TacticAst.Command (_, cmd) -> + print_endline (TacticAstPp.pp_command cmd) + | TacticAst.Tactical (_, tac) -> + print_endline (TacticAstPp.pp_tactical tac)) +(* | `Tactical -> let tac = CicTextualParser2.parse_tactical istream in print_endline (pp_tactical tac) +*) | `Alias -> let env = CicTextualParser2.EnvironmentP3.of_string line in print_endline (CicTextualParser2.EnvironmentP3.to_string env) diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml index 128da869b..6bfced57e 100644 --- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml +++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml @@ -367,9 +367,9 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = function [] -> [] | (Some (n,C.Decl t))::tl -> - (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl) + (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl) | (Some (n,C.Def (t,None)))::tl -> - (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None))):: + (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None))):: (aux (i+1) tl) | None::tl -> None::(aux (i+1) tl) | (Some (_,C.Def (_,Some _)))::_ -> assert false @@ -398,7 +398,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = in let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in (* Checks suppressed *) - CicSubstitution.lift_meta l ty + CicSubstitution.subst_meta l ty | C.Sort (C.Type t) -> (* TASSI: CONSTRAINT *) C.Sort (C.Type (CicUniv.fresh())) | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())) (* TASSI: CONSTRAINT *) diff --git a/helm/ocaml/cic_proof_checking/.depend b/helm/ocaml/cic_proof_checking/.depend index c212f6cad..09359d63a 100644 --- a/helm/ocaml/cic_proof_checking/.depend +++ b/helm/ocaml/cic_proof_checking/.depend @@ -1,19 +1,15 @@ cicLogger.cmo: cicLogger.cmi cicLogger.cmx: cicLogger.cmi -cicEnvironment.cmo: cicLogger.cmi cicEnvironment.cmi -cicEnvironment.cmx: cicLogger.cmx cicEnvironment.cmi -cicUnivUtils.cmo: cicEnvironment.cmi cicUnivUtils.cmi -cicUnivUtils.cmx: cicEnvironment.cmx cicUnivUtils.cmi +cicEnvironment.cmo: cicEnvironment.cmi +cicEnvironment.cmx: cicEnvironment.cmi cicPp.cmo: cicEnvironment.cmi cicPp.cmi cicPp.cmx: cicEnvironment.cmx cicPp.cmi +cicUnivUtils.cmo: cicEnvironment.cmi cicUnivUtils.cmi +cicUnivUtils.cmx: cicEnvironment.cmx cicUnivUtils.cmi cicSubstitution.cmo: cicEnvironment.cmi cicSubstitution.cmi cicSubstitution.cmx: cicEnvironment.cmx cicSubstitution.cmi cicMiniReduction.cmo: cicSubstitution.cmi cicMiniReduction.cmi cicMiniReduction.cmx: cicSubstitution.cmx cicMiniReduction.cmi -cicReductionNaif.cmo: cicSubstitution.cmi cicPp.cmi cicEnvironment.cmi \ - cicReductionNaif.cmi -cicReductionNaif.cmx: cicSubstitution.cmx cicPp.cmx cicEnvironment.cmx \ - cicReductionNaif.cmi cicReduction.cmo: cicSubstitution.cmi cicPp.cmi cicEnvironment.cmi \ cicReduction.cmi cicReduction.cmx: cicSubstitution.cmx cicPp.cmx cicEnvironment.cmx \ @@ -22,5 +18,7 @@ cicTypeChecker.cmo: cicSubstitution.cmi cicReduction.cmi cicPp.cmi \ cicLogger.cmi cicEnvironment.cmi cicTypeChecker.cmi cicTypeChecker.cmx: cicSubstitution.cmx cicReduction.cmx cicPp.cmx \ cicLogger.cmx cicEnvironment.cmx cicTypeChecker.cmi -cicElim.cmo: cicSubstitution.cmi cicEnvironment.cmi cicElim.cmi -cicElim.cmx: cicSubstitution.cmx cicEnvironment.cmx cicElim.cmi +cicElim.cmo: cicTypeChecker.cmi cicSubstitution.cmi cicReduction.cmi \ + cicPp.cmi cicEnvironment.cmi cicElim.cmi +cicElim.cmx: cicTypeChecker.cmx cicSubstitution.cmx cicReduction.cmx \ + cicPp.cmx cicEnvironment.cmx cicElim.cmi diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile index 95657131f..de106143c 100644 --- a/helm/ocaml/cic_proof_checking/Makefile +++ b/helm/ocaml/cic_proof_checking/Makefile @@ -12,7 +12,6 @@ INTERFACE_FILES = \ cicUnivUtils.mli \ cicSubstitution.mli \ cicMiniReduction.mli \ - cicReductionNaif.mli \ cicReduction.mli \ cicTypeChecker.mli \ cicElim.mli @@ -34,14 +33,6 @@ all_utilities: opt_utilities: $(MAKE) -C utilities/ opt -cicReduction.ml: $(REDUCTION_IMPLEMENTATION) - if ! [ -f $@ ]; then \ - echo "Using $< for $@"; \ - ln -s $< $@; \ - else \ - true; \ - fi - clean: clean_utilities clean_utilities: $(MAKE) -C utilities/ clean diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli index fe87fc4af..ce6a7f225 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli @@ -83,7 +83,7 @@ val add_type_checked_term : UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit (** remove a type checked object - * @raise Term_not_found when given term is not in the environment + * @raise Object_not_found when given term is not in the environment * @raise Failure when remove_term is invoked while type checking *) val remove_obj: UriManager.uri -> unit diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml similarity index 99% rename from helm/ocaml/cic_proof_checking/cicReductionMachine.ml rename to helm/ocaml/cic_proof_checking/cicReduction.ml index 0610504c4..687a46549 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml +++ b/helm/ocaml/cic_proof_checking/cicReduction.ml @@ -560,7 +560,7 @@ if List.mem uri params then prerr_endline "---- OK2" ; | (k, e, ens, (C.Meta (n,l) as t), s) -> (try let (_, term,_) = CicUtil.lookup_subst n subst in - reduce (k, e, ens,CicSubstitution.lift_meta l term,s) + reduce (k, e, ens,CicSubstitution.subst_meta l term,s) with CicUtil.Subst_not_found _ -> let t' = unwind k e ens t in if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))) diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.mli b/helm/ocaml/cic_proof_checking/cicReductionMachine.mli deleted file mode 100644 index 7e36a05d2..000000000 --- a/helm/ocaml/cic_proof_checking/cicReductionMachine.mli +++ /dev/null @@ -1,33 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -exception WrongUriToInductiveDefinition -exception ReferenceToConstant -exception ReferenceToVariable -exception ReferenceToCurrentProof -exception ReferenceToInductiveDefinition -val fdebug : int ref -val whd : Cic.context -> Cic.term -> Cic.term -val are_convertible : Cic.context -> Cic.term -> Cic.term -> CicUniv.universe_graph -> bool * CicUniv.universe_graph diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml deleted file mode 100644 index 04067ccbf..000000000 --- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml +++ /dev/null @@ -1,407 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -exception CicReductionInternalError;; -exception WrongUriToInductiveDefinition;; - -let fdebug = ref 1;; -let debug t env s = - let rec debug_aux t i = - let module C = Cic in - let module U = UriManager in - CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i - in - if !fdebug = 0 then - prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "") -;; - -exception Impossible of int;; -exception ReferenceToConstant;; -exception ReferenceToVariable;; -exception ReferenceToCurrentProof;; -exception ReferenceToInductiveDefinition;; -exception RelToHiddenHypothesis;; - -(* takes a well-typed term *) -let whd context = - let rec whdaux l = - let module C = Cic in - let module S = CicSubstitution in - function - C.Rel n as t -> - (match List.nth context (n-1) with - Some (_, C.Decl _) -> if l = [] then t else C.Appl (t::l) - | Some (_, C.Def (bo,_)) -> whdaux l (S.lift n bo) - | None -> raise RelToHiddenHypothesis - ) - | C.Var (uri,exp_named_subst) as t -> - let o,_ = - CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri - in - (match o with - C.Constant _ -> raise ReferenceToConstant - | C.CurrentProof _ -> raise ReferenceToCurrentProof - | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - | C.Variable (_,None,_,_,_) -> if l = [] then t else C.Appl (t::l) - | C.Variable (_,Some body,_,_,_) -> - whdaux l (CicSubstitution.subst_vars exp_named_subst body) - ) - | C.Meta _ as t -> if l = [] then t else C.Appl (t::l) - | C.Sort _ as t -> t (* l should be empty *) - | C.Implicit _ as t -> t - | C.Cast (te,ty) -> whdaux l te (*CSC E' GIUSTO BUTTARE IL CAST? *) - | C.Prod _ as t -> t (* l should be empty *) - | C.Lambda (name,s,t) as t' -> - (match l with - [] -> t' - | he::tl -> whdaux tl (S.subst he t) - (* when name is Anonimous the substitution should be superfluous *) - ) - | C.LetIn (n,s,t) -> whdaux l (S.subst (whdaux [] s) t) - | C.Appl (he::tl) -> whdaux (tl@l) he - | C.Appl [] -> raise (Impossible 1) - | C.Const (uri,exp_named_subst) as t -> - let o,_ = - CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri - in - (match o with - C.Constant (_,Some body,_,_,_) -> - whdaux l (CicSubstitution.subst_vars exp_named_subst body) - | C.Constant _ -> if l = [] then t else C.Appl (t::l) - | C.Variable _ -> raise ReferenceToVariable - | C.CurrentProof (_,_,body,_,_,_) -> - whdaux l (CicSubstitution.subst_vars exp_named_subst body) - | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - ) - | C.MutInd _ as t -> if l = [] then t else C.Appl (t::l) - | C.MutConstruct _ as t -> if l = [] then t else C.Appl (t::l) - | C.MutCase (mutind,i,_,term,pl) as t-> - let decofix = - function - C.CoFix (i,fl) as t -> - let (_,_,body) = List.nth fl i in - let body' = - let counter = ref (List.length fl) in - List.fold_right - (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) - fl - body - in - whdaux [] body' - | C.Appl (C.CoFix (i,fl) :: tl) -> - let (_,_,body) = List.nth fl i in - let body' = - let counter = ref (List.length fl) in - List.fold_right - (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) - fl - body - in - whdaux tl body' - | t -> t - in - (match decofix (whdaux [] term) with - C.MutConstruct (_,_,j,_) -> whdaux l (List.nth pl (j-1)) - | C.Appl (C.MutConstruct (_,_,j,_) :: tl) -> - let (arity, r) = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in - match o with - C.InductiveDefinition (tl,ingredients,r,_) -> - let (_,_,arity,_) = List.nth tl i in - (arity,r) - | _ -> raise WrongUriToInductiveDefinition - in - let ts = - let rec eat_first = - function - (0,l) -> l - | (n,he::tl) when n > 0 -> eat_first (n - 1, tl) - | _ -> raise (Impossible 5) - in - eat_first (r,tl) - in - whdaux (ts@l) (List.nth pl (j-1)) - | C.Cast _ | C.Implicit _ -> - raise (Impossible 2) (* we don't trust our whd ;-) *) - | _ -> if l = [] then t else C.Appl (t::l) - ) - | C.Fix (i,fl) as t -> - let (_,recindex,_,body) = List.nth fl i in - let recparam = - try - Some (List.nth l recindex) - with - _ -> None - in - (match recparam with - Some recparam -> - (match whdaux [] recparam with - C.MutConstruct _ - | C.Appl ((C.MutConstruct _)::_) -> - let body' = - let counter = ref (List.length fl) in - List.fold_right - (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl))) - fl - body - in - (* Possible optimization: substituting whd recparam in l *) - whdaux l body' - | _ -> if l = [] then t else C.Appl (t::l) - ) - | None -> if l = [] then t else C.Appl (t::l) - ) - | C.CoFix (i,fl) as t -> - if l = [] then t else C.Appl (t::l) - in -(*CSC -function t -> -prerr_endline ("PRIMA WHD" ^ CicPp.ppterm t) ; flush stderr ; -List.iter (function (Cic.Decl t) -> prerr_endline ("Context: " ^ CicPp.ppterm t) | (Cic.Def t) -> prerr_endline ("Context:= " ^ CicPp.ppterm t)) context ; flush stderr ; prerr_endline " (n1 = n2),ugraph - | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) -> - let b = U.eq uri1 uri2 in - if b then - (try - List.fold_right2 - (fun (uri1,x) (uri2,y) (b,ugraph) -> - (* FIXME: lazy! *) - let b',ugraph' = aux test_equality_only context x y ugraph in - (U.eq uri1 uri2 && b' && b),ugraph' - ) exp_named_subst1 exp_named_subst2 (true,ugraph) - with - Invalid_argument _ -> false,ugraph - ) - else - false,ugraph - | (C.Meta (n1,l1), C.Meta (n2,l2)) -> - let b = n1 = n2 in - if b then - List.fold_left2 - (fun (b,ugraph) t1 t2 -> - if b then - match t1,t2 with - None,_ - | _,None -> true,ugraph - | Some t1',Some t2' -> - aux test_equality_only context t1' t2' ugraph - else - false,ugraph - ) (true,ugraph) l1 l2 - else - false,ugraph - (* TASSI: CONSTRAINTS *) - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only -> - true,(CicUniv.add_eq t2 t1 ugraph) - (* TASSI: CONSTRAINTS *) - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> - true,(CicUniv.add_ge t2 t1 ugraph) - (* TASSI: CONSTRAINTS *) - | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph - (* TASSI: CONSTRAINTS *) - | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph - | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> - let b',ugraph' = aux true context s1 s2 ugraph in - if b' then - aux test_equality_only ((Some (name1, (C.Decl s1)))::context) - t1 t2 ugraph' - else - false,ugraph - | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) -> - let b',ugraph' = aux test_equality_only context s1 s2 ugraph in - if b' then - aux test_equality_only ((Some (name1, (C.Decl s1)))::context) - t1 t2 ugraph' - else - false,ugraph - | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) -> - let b',ugraph' = aux test_equality_only context s1 s2 ugraph in - if b' then - aux test_equality_only - ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph' - else - false,ugraph - | (C.Appl l1, C.Appl l2) -> - (try - List.fold_right2 - (fun x y (b,ugraph) -> - if b then - aux test_equality_only context x y ugraph - else - false,ugraph) l1 l2 (true,ugraph) - with - Invalid_argument _ -> false,ugraph - ) - | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) -> - let b' = U.eq uri1 uri2 in - if b' then - (try - List.fold_right2 - (fun (uri1,x) (uri2,y) (b,ugraph) -> - if b && U.eq uri1 uri2 then - aux test_equality_only context x y ugraph - else - false,ugraph - ) exp_named_subst1 exp_named_subst2 (true,ugraph) - with - Invalid_argument _ -> false,ugraph - ) - else - false,ugraph - | (C.MutInd (uri1,i1,exp_named_subst1), - C.MutInd (uri2,i2,exp_named_subst2) - ) -> - let b' = U.eq uri1 uri2 && i1 = i2 in - if b' then - (try - List.fold_right2 - (fun (uri1,x) (uri2,y) (b,ugraph) -> - if b && U.eq uri1 uri2 then - aux test_equality_only context x y ugraph - else - false,ugraph - ) exp_named_subst1 exp_named_subst2 (true,ugraph) - with - Invalid_argument _ -> false,ugraph - ) - else - false,ugraph - | (C.MutConstruct (uri1,i1,j1,exp_named_subst1), - C.MutConstruct (uri2,i2,j2,exp_named_subst2) - ) -> - let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in - if b' then - (try - List.fold_right2 - (fun (uri1,x) (uri2,y) (b,ugraph) -> - if b && U.eq uri1 uri2 then - aux test_equality_only context x y ugraph - else - false,ugraph - ) exp_named_subst1 exp_named_subst2 (true,ugraph) - with - Invalid_argument _ -> false,ugraph - ) - else - false,ugraph - | (C.MutCase (uri1,i1,outtype1,term1,pl1), - C.MutCase (uri2,i2,outtype2,term2,pl2)) -> - let b' = U.eq uri1 uri2 && i1 = i2 in - if b' then - let b'',ugraph''=aux test_equality_only context - outtype1 outtype2 ugraph in - if b'' then - let b''',ugraph'''= aux test_equality_only context - term1 term2 ugraph'' in - List.fold_right2 - (fun x y (b,ugraph) -> - if b then - aux test_equality_only context x y ugraph - else - false,ugraph) - pl1 pl2 (true,ugraph''') - else - false,ugraph - else - false,ugraph - | (C.Fix (i1,fl1), C.Fix (i2,fl2)) -> - let tys = - List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1 - in - if i1 = i2 then - List.fold_right2 - (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) -> - if b && recindex1 = recindex2 then - let b',ugraph' = aux test_equality_only context ty1 ty2 - ugraph in - if b' then - aux test_equality_only (tys@context) bo1 bo2 ugraph' - else - false,ugraph - else - false,ugraph) - fl1 fl2 (true,ugraph) - else - false,ugraph - | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) -> - let tys = - List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1 - in - if i1 = i2 then - List.fold_right2 - (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) -> - if b then - let b',ugraph' = aux test_equality_only context ty1 ty2 - ugraph in - if b' then - aux test_equality_only (tys@context) bo1 bo2 ugraph' - else - false,ugraph - else - false,ugraph) - fl1 fl2 (true,ugraph) - else - false,ugraph - | (C.Cast _, _) | (_, C.Cast _) - | (C.Implicit _, _) | (_, C.Implicit _) -> - assert false - | (_,_) -> false,ugraph - end - in - let b,ugraph' = aux2 test_equality_only t1 t2 ugraph in - if b then - b,ugraph' - else - begin - debug t1 [t2] "PREWHD"; - let t1' = whd context t1 in - let t2' = whd context t2 in - debug t1' [t2'] "POSTWHD"; - aux2 test_equality_only t1' t2' ugraph - end - in - aux false c t1 t2 ugraph -;; diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.mli b/helm/ocaml/cic_proof_checking/cicReductionNaif.mli deleted file mode 100644 index 624eebf5d..000000000 --- a/helm/ocaml/cic_proof_checking/cicReductionNaif.mli +++ /dev/null @@ -1,35 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -exception WrongUriToInductiveDefinition -exception ReferenceToConstant -exception ReferenceToVariable -exception ReferenceToCurrentProof -exception ReferenceToInductiveDefinition -val fdebug : int ref -val whd : Cic.context -> Cic.term -> Cic.term -val are_convertible : - Cic.context -> Cic.term -> Cic.term -> - CicUniv.universe_graph -> bool * CicUniv.universe_graph diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml index cd9773160..30a24c13a 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml @@ -417,10 +417,10 @@ if List.mem uri params then prerr_endline "---- OK2" ; substaux 1 ;; -(* lift_meta [t_1 ; ... ; t_n] t *) +(* subst_meta [t_1 ; ... ; t_n] t *) (* returns the term [t] where [Rel i] is substituted with [t_i] *) (* [t_i] is lifted as usual when it crosses an abstraction *) -let lift_meta l t = +let subst_meta l t = let module C = Cic in if l = [] then t else let rec aux k = function diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.mli b/helm/ocaml/cic_proof_checking/cicSubstitution.mli index 1f0705881..b1c09277b 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.mli +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.mli @@ -52,10 +52,8 @@ val subst : Cic.term -> Cic.term -> Cic.term val subst_vars : Cic.term Cic.explicit_named_substitution -> Cic.term -> Cic.term -(* TODO CSC rename to subst_meta *) - -(* lift_meta [t_1 ; ... ; t_n] t *) +(* subst_meta [t_1 ; ... ; t_n] t *) (* returns the term [t] where [Rel i] is substituted with [t_i] *) (* [t_i] is lifted as usual when it crosses an abstraction *) -val lift_meta : (Cic.term option) list -> Cic.term -> Cic.term +val subst_meta : (Cic.term option) list -> Cic.term -> Cic.term diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 2a7f8c4ae..fe46e4748 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -1395,12 +1395,12 @@ and check_metasenv_consistency ~logger ?(subst=[]) metasenv context function [] -> [] | (Some (n,C.Decl t))::tl -> - (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl) + (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl) | (Some (n,C.Def (t,None)))::tl -> - (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl) + (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl) | None::tl -> None::(aux (i+1) tl) | (Some (n,C.Def (t,Some ty)))::tl -> - (Some (n,C.Def ((S.lift_meta l (S.lift i t)),Some (S.lift_meta l (S.lift i ty)))))::(aux (i+1) tl) + (Some (n,C.Def ((S.subst_meta l (S.lift i t)),Some (S.subst_meta l (S.lift i ty)))))::(aux (i+1) tl) in aux 1 canonical_context in @@ -1482,15 +1482,15 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = ~subst metasenv context canonical_context l ugraph in (* assuming subst is well typed !!!!! *) - ((CicSubstitution.lift_meta l ty), ugraph1) - (* type_of_aux context (CicSubstitution.lift_meta l term) *) + ((CicSubstitution.subst_meta l ty), ugraph1) + (* type_of_aux context (CicSubstitution.subst_meta l term) *) with CicUtil.Subst_not_found _ -> let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in let ugraph1 = check_metasenv_consistency ~logger ~subst metasenv context canonical_context l ugraph in - ((CicSubstitution.lift_meta l ty),ugraph1)) + ((CicSubstitution.subst_meta l ty),ugraph1)) (* TASSI: CONSTRAINTS *) | C.Sort (C.Type t) -> let t' = CicUniv.fresh() in diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index eae88a14d..809c57dfe 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -33,52 +33,52 @@ type 'term pattern = [ `Goal | `Everywhere ] (* when an 'ident option is None, the default is to apply the tactic to the current goal *) -type ('term, 'ident) tactic = - | LocatedTactic of CicAst.location * ('term, 'ident) tactic +type loc = CicAst.location - | Absurd of 'term - | Apply of 'term - | Auto - | Assumption - | Change of 'term * 'term * 'ident option (* what, with what, where *) - | Change_pattern of 'term pattern * 'term * 'ident option +type ('term, 'ident) tactic = + | Absurd of loc * 'term + | Apply of loc * 'term + | Auto of loc + | Assumption of loc + | Change of loc * 'term * 'term * 'ident option (* what, with what, where *) + | Change_pattern of loc * 'term pattern * 'term * 'ident option (* what, with what, where *) - | Contradiction - | Cut of 'term - | Decompose of 'ident * 'ident list (* where, which principles *) - | Discriminate of 'ident - | Elim of 'term * 'term option (* what to elim, which principle to use *) - | ElimType of 'term - | Exact of 'term - | Exists - | Fold of reduction_kind * 'term - | Fourier - | Hint - | Injection of 'ident - | Intros of int option * 'ident list - | Left - | LetIn of 'term * 'ident -(* | Named_intros of 'ident list (* joined with Intros above *) *) -(* | Reduce of reduction_kind * 'term pattern * 'ident option (* what, where *) *) - | Reduce of reduction_kind * ('term list * 'term pattern) option + | Contradiction of loc + | Cut of loc * 'term + | Decompose of loc * 'ident * 'ident list (* where, which principles *) + | Discriminate of loc * 'ident + | Elim of loc * 'term * 'term option (* what to elim, which principle to use *) + | ElimType of loc * 'term + | Exact of loc * 'term + | Exists of loc + | Fold of loc * reduction_kind * 'term + | Fourier of loc + | Goal of loc * int (* change current goal, argument is goal number 1-based *) + | Hint of loc + | Injection of loc * 'ident + | Intros of loc * int option * 'ident list + | Left of loc + | LetIn of loc * 'term * 'ident +(* | Named_intros of loc * 'ident list (* joined with Intros above *) *) +(* | Reduce of loc * reduction_kind * 'term pattern * 'ident option (* what, where *) *) + | Reduce of loc * reduction_kind * ('term list * 'term pattern) option (* kind, (what, where) * if second argument is None, reduction is applied to the current goal, - * otherwise to each occurrence of terms given in list occuring in term + * otherwise to each occurrence of loc * terms given in list occuring in term * pattern *) - | Reflexivity - | Replace of 'term * 'term (* what, with what *) - | Replace_pattern of 'term pattern * 'term - | Rewrite of direction * 'term * 'ident option - | Right - | Ring - | Split - | Symmetry - | Transitivity of 'term + | Reflexivity of loc + | Replace of loc * 'term * 'term (* what, with what *) + | Replace_pattern of loc * 'term pattern * 'term + | Rewrite of loc * direction * 'term * 'ident option + | Right of loc + | Ring of loc + | Split of loc + | Symmetry of loc + | Transitivity of loc * 'term type thm_flavour = [ `Definition | `Fact - | `Goal | `Lemma | `Remark | `Theorem @@ -92,46 +92,57 @@ type search_kind = [ `Locate | `Hint | `Match | `Elim ] type print_kind = [ `Env | `Coer ] +type 'term macro = + | Abort of loc + | Print of loc * string + | Check of loc * 'term + | Quit of loc + | Redo of loc * int option + | Undo of loc * int option +(* | Print of loc * print_kind *) + | Search_pat of loc * search_kind * string (* searches with string pattern *) + | Search_term of loc * search_kind * 'term (* searches with term pattern *) + +type alias_spec = + | Ident_alias of string * string (* identifier, uri *) + | Symbol_alias of string * int * string (* name, instance no, description *) + | Number_alias of int * string (* instance no, description *) + type 'term command = - | Abort - | Baseuri of string option (** get/set base uri *) - | Basedir of string option (** get/set base dir *) - | Check of 'term - | Search_pat of search_kind * string (* searches with string pattern *) - | Search_term of search_kind * 'term (* searches with term pattern *) - | Proof - | Qed of string option + | Set of loc * string * string + | Qed of loc (** name. * Name is needed when theorem was started without providing a name *) - | Quit - | Inductive of (string * 'term) list * 'term inductive_type list - (** parameters, list of mutual inductive types *) - | Theorem of thm_flavour * string option * 'term * 'term option + | Inductive of loc * (string * 'term) list * 'term inductive_type list + (** parameters, list of loc * mutual inductive types *) + | Theorem of loc * thm_flavour * string option * 'term * 'term option (** flavour, name, type, body * - name is absent when an unnamed theorem is being proved, tipically in * interactive usage * - body is present when its given along with the command, otherwise it * will be given in proof editing mode using the tactical language *) - | Coercion of 'term - | Redo of int option - | Undo of int option - | Print of print_kind + | Coercion of loc * 'term + | Alias of loc * alias_spec type ('term, 'ident) tactical = - | LocatedTactical of CicAst.location * ('term, 'ident) tactical - - | Tactic of ('term, 'ident) tactic - | Command of 'term command + | Tactic of loc * ('term, 'ident) tactic + | Fail of loc + | Do of loc * int * ('term, 'ident) tactical + | IdTac of loc + | Repeat of loc * ('term, 'ident) tactical + | Seq of loc * ('term, 'ident) tactical list (* sequential composition *) + | Then of loc * ('term, 'ident) tactical * ('term, 'ident) tactical list + | Tries of loc * ('term, 'ident) tactical list + (* try a sequence of loc * tacticals until one succeeds, fail otherwise *) + | Try of loc * ('term, 'ident) tactical (* try a tactical and mask failures *) - | Fail - | Do of int * ('term, 'ident) tactical - | IdTac - | Repeat of ('term, 'ident) tactical - | Seq of ('term, 'ident) tactical list (* sequential composition *) - | Then of ('term, 'ident) tactical * ('term, 'ident) tactical list - | Tries of ('term, 'ident) tactical list - (* try a sequence of tacticals until one succeeds, fail otherwise *) - | Try of ('term, 'ident) tactical (* try a tactical and mask failures *) +type ('term, 'ident) statement = + | Command of loc * 'term command + | Macro of loc * 'term macro + (* Macro are substantially queries, but since we are not the kind of + * peolpe that like to push "start" to turn off the computer + * we added this command *) + | Tactical of loc * ('term, 'ident) tactical diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml index 80e3effce..74a6a749e 100644 --- a/helm/ocaml/cic_transformations/tacticAst2Box.ml +++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml @@ -39,57 +39,57 @@ open TacticAst let rec count_tactic current_size tac = if current_size > maxsize then current_size else match tac with - LocatedTactic (_, tac) -> count_tactic current_size tac - | Absurd term -> countterm (current_size + 6) term - | Apply term -> countterm (current_size + 6) term - | Auto -> current_size + 4 - | Assumption -> current_size + 10 - | Change (t1, t2, where) -> + | Absurd (_, term) -> countterm (current_size + 6) term + | Apply (_, term) -> countterm (current_size + 6) term + | Auto _ -> current_size + 4 + | Assumption _ -> current_size + 10 + | Change (_, t1, t2, where) -> let size1 = countterm (current_size + 12) t1 in (* change, with *) let size2 = countterm size1 t2 in (match where with None -> size2 | Some ident -> size2 + 3 + String.length ident) - | Change_pattern (_, _, _) -> assert false (* TODO *) - | Contradiction -> current_size + 13 - | Cut term -> countterm (current_size + 4) term - | Decompose (ident, principles) -> + | Change_pattern _ -> assert false (* TODO *) + | Contradiction _ -> current_size + 13 + | Cut (_, term) -> countterm (current_size + 4) term + | Decompose (_, ident, principles) -> List.fold_left (fun size s -> size + (String.length s)) (current_size + 11 + String.length ident) principles - | Discriminate ident -> current_size + 12 + (String.length ident) - | Elim (term, using) -> + | Discriminate (_, ident) -> current_size + 12 + (String.length ident) + | Elim (_, term, using) -> let size1 = countterm (current_size + 5) term in (match using with None -> size1 | Some term -> countterm (size1 + 7) term) - | ElimType term -> countterm (current_size + 10) term - | Exact term -> countterm (current_size + 6) term - | Exists -> current_size + 6 - | Fold (kind, term) -> + | ElimType (_, term) -> countterm (current_size + 10) term + | Exact (_, term) -> countterm (current_size + 6) term + | Exists _ -> current_size + 6 + | Fold (_, kind, term) -> countterm (current_size + 5) term - | Fourier -> current_size + 7 - | Hint -> current_size + 4 - | Injection ident -> current_size + 10 + (String.length ident) - | Intros (num, idents) -> + | Fourier _ -> current_size + 7 + | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n))) + | Hint _ -> current_size + 4 + | Injection (_, ident) -> current_size + 10 + (String.length ident) + | Intros (_, num, idents) -> List.fold_left (fun size s -> size + (String.length s)) (current_size + 7) idents - | Left -> current_size + 4 - | LetIn (term, ident) -> + | Left _ -> current_size + 4 + | LetIn (_, term, ident) -> countterm (current_size + 5 + String.length ident) term - | Reduce (_, _) -> assert false (* TODO *) - | Reflexivity -> current_size + 11 - | Replace (t1, t2) -> + | Reduce _ -> assert false (* TODO *) + | Reflexivity _ -> current_size + 11 + | Replace (_, t1, t2) -> let size1 = countterm (current_size + 14) t1 in (* replace, with *) countterm size1 t2 - | Replace_pattern (_, _) -> assert false (* TODO *) - | Rewrite (_, _, _) -> assert false (* TODO *) - | Right -> current_size + 5 - | Ring -> current_size + 4 - | Split -> current_size + 5 - | Symmetry -> current_size + 8 - | Transitivity term -> + | Replace_pattern _ -> assert false (* TODO *) + | Rewrite _ -> assert false (* TODO *) + | Right _ -> current_size + 5 + | Ring _ -> current_size + 4 + | Split _ -> current_size + 5 + | Symmetry _ -> current_size + 8 + | Transitivity (_, term) -> countterm (current_size + 13) term ;; @@ -126,17 +126,15 @@ let rec tactic2box tac = small_tactic2box tac and big_tactic2box = function - LocatedTactic (loc, tac) -> - big_tactic2box tac - | Absurd term -> + | Absurd (_, term) -> Box.V([],[Box.Text([],"absurd"); ast2astBox term]) - | Apply term -> + | Apply (_, term) -> Box.V([],[Box.Text([],"apply"); ast2astBox term]) - | Assumption -> Box.Text([],"assumption") - | Auto -> Box.Text([],"auto") - | Change (t1, t2, where) -> + | Assumption _ -> Box.Text([],"assumption") + | Auto _ -> Box.Text([],"auto") + | Change (_, t1, t2, where) -> let where = (match where with None -> [] @@ -151,12 +149,12 @@ and big_tactic2box = function (pretty_append [Box.Text([],"with")] t2)@where) - | Change_pattern (_, _, _) -> assert false (* TODO *) - | Contradiction -> Box.Text([],"contradiction") - | Cut term -> + | Change_pattern _ -> assert false (* TODO *) + | Contradiction _ -> Box.Text([],"contradiction") + | Cut (_, term) -> Box.V([],[Box.Text([],"cut"); Box.indent(ast2astBox term)]) - | Decompose (ident, principles) -> + | Decompose (_, ident, principles) -> let principles = List.map (fun x -> Box.Text([],x)) principles in Box.V([],[Box.Text([],"decompose"); @@ -164,10 +162,10 @@ and big_tactic2box = function Box.V([],principles); Box.Text([],"]")]); Box.Text([],ident)]) - | Discriminate ident -> + | Discriminate (_, ident) -> Box.V([],[Box.Text([],"discriminate"); Box.Text([],ident)]) - | Elim (term, using) -> + | Elim (_, term, using) -> let using = (match using with None -> [] @@ -179,24 +177,25 @@ and big_tactic2box = function (pretty_append [Box.Text([],"elim")] term)@using) - | ElimType term -> + | ElimType (_, term) -> Box.V([],[Box.Text([],"elim type"); Box.indent(ast2astBox term)]) - | Exact term -> + | Exact (_, term) -> Box.V([],[Box.Text([],"exact"); Box.indent(ast2astBox term)]) - | Exists -> Box.Text([],"exists") - | Fold (kind, term) -> + | Exists _ -> Box.Text([],"exists") + | Fold (_, kind, term) -> Box.V([],[Box.H([],[Box.Text([],"fold"); Box.smallskip; Box.Text([],string_of_kind kind)]); Box.indent(ast2astBox term)]) - | Fourier -> Box.Text([],"fourier") - | Hint -> Box.Text([],"hint") - | Injection ident -> + | Fourier _ -> Box.Text([],"fourier") + | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n) + | Hint _ -> Box.Text([],"hint") + | Injection (_, ident) -> Box.V([],[Box.Text([],"transitivity"); Box.indent (Box.Text([],ident))]) - | Intros (num, idents) -> + | Intros (_, num, idents) -> let num = (match num with None -> [] @@ -206,17 +205,17 @@ and big_tactic2box = function Box.V([],[Box.Text([],"decompose"); Box.H([],[Box.smallskip; Box.V([],idents)])]) - | Left -> Box.Text([],"left") - | LetIn (term, ident) -> + | Left _ -> Box.Text([],"left") + | LetIn (_, term, ident) -> Box.V([],[Box.H([],[Box.Text([],"let"); Box.smallskip; Box.Text([],ident); Box.smallskip; Box.Text([],"=")]); Box.indent (ast2astBox term)]) - | Reduce (_, _) -> assert false (* TODO *) - | Reflexivity -> Box.Text([],"reflexivity") - | Replace (t1, t2) -> + | Reduce _ -> assert false (* TODO *) + | Reflexivity _ -> Box.Text([],"reflexivity") + | Replace (_, t1, t2) -> Box.V([], (pretty_append [Box.Text([],"replace")] @@ -224,13 +223,13 @@ and big_tactic2box = function (pretty_append [Box.Text([],"with")] t2)) - | Replace_pattern (_, _) -> assert false (* TODO *) - | Rewrite (_, _, _) -> assert false (* TODO *) - | Right -> Box.Text([],"right") - | Ring -> Box.Text([],"ring") - | Split -> Box.Text([],"split") - | Symmetry -> Box.Text([],"symmetry") - | Transitivity term -> + | Replace_pattern _ -> assert false (* TODO *) + | Rewrite _ -> assert false (* TODO *) + | Right _ -> Box.Text([],"right") + | Ring _ -> Box.Text([],"ring") + | Split _ -> Box.Text([],"split") + | Symmetry _ -> Box.Text([],"symmetry") + | Transitivity (_, term) -> Box.V([],[Box.Text([],"transitivity"); Box.indent (ast2astBox term)]) ;; @@ -238,35 +237,35 @@ and big_tactic2box = function open TacticAst let rec tactical2box = function - | LocatedTactical (loc, tac) -> tactical2box tac - - | Tactic tac -> tactic2box tac + | Tactic (_, tac) -> tactic2box tac +(* | Command cmd -> (* TODO dummy implementation *) Box.Text([], TacticAstPp.pp_tactical (Command cmd)) +*) - | Fail -> Box.Text([],"fail") - | Do (count, tac) -> + | Fail _ -> Box.Text([],"fail") + | Do (_, count, tac) -> Box.V([],[Box.Text([],"do " ^ string_of_int count); Box.indent (tactical2box tac)]) - | IdTac -> Box.Text([],"id") - | Repeat tac -> + | IdTac _ -> Box.Text([],"id") + | Repeat (_, tac) -> Box.V([],[Box.Text([],"repeat"); Box.indent (tactical2box tac)]) - | Seq tacs -> + | Seq (_, tacs) -> Box.V([],tacticals2box tacs) - | Then (tac, tacs) -> + | Then (_, tac, tacs) -> Box.V([],[tactical2box tac; Box.H([],[Box.skip; Box.Text([],"["); Box.V([],tacticals2box tacs); Box.Text([],"]");])]) - | Tries tacs -> + | Tries (_, tacs) -> Box.V([],[Box.Text([],"try"); Box.H([],[Box.skip; Box.Text([],"["); Box.V([],tacticals2box tacs); Box.Text([],"]");])]) - | Try tac -> + | Try (_, tac) -> Box.V([],[Box.Text([],"try"); Box.indent (tactical2box tac)]) diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 0d539ddbe..1a28fa578 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -28,9 +28,11 @@ open Printf open TacticAst let tactical_terminator = "." +let tactic_terminator = tactical_terminator let tactical_separator = ";" -let pp_term term = CicAstPp.pp_term term +let pp_term_ast term = CicAstPp.pp_term term +let pp_term_cic term = CicPp.ppterm term let pp_idents idents = "[" ^ String.concat "; " idents ^ "]" @@ -40,57 +42,58 @@ let pp_reduction_kind = function | `Whd -> "whd" let rec pp_tactic = function - | LocatedTactic (loc, tac) -> pp_tactic tac - | Absurd term -> "absurd" ^ pp_term term - | Apply term -> "apply " ^ pp_term term - | Auto -> "auto" - | Assumption -> "assumption" - | Change (t1, t2, where) -> - sprintf "change %s with %s%s" (pp_term t1) (pp_term t2) + | Absurd (_, term) -> "absurd" ^ pp_term_ast term + | Apply (_, term) -> "apply " ^ pp_term_ast term + | Auto _ -> "auto" + | Assumption _ -> "assumption" + | Change (_, t1, t2, where) -> + sprintf "change %s with %s%s" (pp_term_ast t1) (pp_term_ast t2) (match where with None -> "" | Some ident -> "in " ^ ident) - | Change_pattern (_, _, _) -> assert false (* TODO *) - | Contradiction -> "contradiction" - | Cut term -> "cut " ^ pp_term term - | Decompose (ident, principles) -> + | Change_pattern (_, _, _, _) -> assert false (* TODO *) + | Contradiction _ -> "contradiction" + | Cut (_, term) -> "cut " ^ pp_term_ast term + | Decompose (_, ident, principles) -> sprintf "decompose %s %s" (pp_idents principles) ident - | Discriminate ident -> "discriminate " ^ ident - | Elim (term, using) -> - sprintf "elim " ^ pp_term term ^ - (match using with None -> "" | Some term -> " using " ^ pp_term term) - | ElimType term -> "elim type " ^ pp_term term - | Exact term -> "exact " ^ pp_term term - | Exists -> "exists" - | Fold (kind, term) -> - sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term term) - | Fourier -> "fourier" - | Hint -> "hint" - | Injection ident -> "injection " ^ ident - | Intros (None, []) -> "intro" - | Intros (num, idents) -> + | Discriminate (_, ident) -> "discriminate " ^ ident + | Elim (_, term, using) -> + sprintf "elim " ^ pp_term_ast term ^ + (match using with None -> "" | Some term -> " using " ^ pp_term_ast term) + | ElimType (_, term) -> "elim type " ^ pp_term_ast term + | Exact (_, term) -> "exact " ^ pp_term_ast term + | Exists _ -> "exists" + | Fold (_, kind, term) -> + sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term_ast term) + | Goal (_, n) -> "goal " ^ string_of_int n + | Fourier _ -> "fourier" + | Hint _ -> "hint" + | Injection (_, ident) -> "injection " ^ ident + | Intros (_, None, []) -> "intro" + | Intros (_, num, idents) -> sprintf "intros%s%s" (match num with None -> "" | Some num -> " " ^ string_of_int num) (match idents with [] -> "" | idents -> " " ^ pp_idents idents) - | Left -> "left" - | LetIn (term, ident) -> sprintf "let %s in %s" (pp_term term) ident - | Reduce (kind, None) - | Reduce (kind, Some ([], `Goal)) -> pp_reduction_kind kind - | Reduce (kind, Some ([], `Everywhere)) -> + | Left _ -> "left" + | LetIn (_, term, ident) -> sprintf "let %s in %s" (pp_term_ast term) ident + | Reduce (_, kind, None) + | Reduce (_, kind, Some ([], `Goal)) -> pp_reduction_kind kind + | Reduce (_, kind, Some ([], `Everywhere)) -> sprintf "%s in hyp" (pp_reduction_kind kind) - | Reduce (kind, Some (terms, `Goal)) -> + | Reduce (_, kind, Some (terms, `Goal)) -> sprintf "%s %s" (pp_reduction_kind kind) - (String.concat ", " (List.map pp_term terms)) - | Reduce (kind, Some (terms, `Everywhere)) -> + (String.concat ", " (List.map pp_term_ast terms)) + | Reduce (_, kind, Some (terms, `Everywhere)) -> sprintf "%s in hyp %s" (pp_reduction_kind kind) - (String.concat ", " (List.map pp_term terms)) - | Reflexivity -> "reflexivity" - | Replace (t1, t2) -> sprintf "replace %s with %s" (pp_term t1) (pp_term t2) - | Replace_pattern (_, _) -> assert false (* TODO *) - | Rewrite (_, _, _) -> assert false (* TODO *) - | Right -> "right" - | Ring -> "ring" - | Split -> "split" - | Symmetry -> "symmetry" - | Transitivity term -> "transitivity " ^ pp_term term + (String.concat ", " (List.map pp_term_ast terms)) + | Reflexivity _ -> "reflexivity" + | Replace (_, t1, t2) -> + sprintf "replace %s with %s" (pp_term_ast t1) (pp_term_ast t2) + | Replace_pattern (_, _, _) -> assert false (* TODO *) + | Rewrite (_, _, _, _) -> assert false (* TODO *) + | Right _ -> "right" + | Ring _ -> "ring" + | Split _ -> "split" + | Symmetry _ -> "symmetry" + | Transitivity (_, term) -> "transitivity " ^ pp_term_ast term let pp_flavour = function | `Definition -> "Definition" @@ -106,38 +109,51 @@ let pp_search_kind = function | `Match -> "match" | `Elim -> "elim" -let pp_command = function - | Abort -> "Abort" - | Baseuri (Some uri) -> sprintf "Baseuri \"%s\"" uri - | Baseuri None -> "Baseuri" - | Check term -> sprintf "Check %s" (pp_term term) - | Proof -> "Proof" - | Qed name -> - (match name with None -> "Qed" | Some name -> sprintf "Save %s" name) - | Quit -> "Quit" - | Redo None -> "Redo" - | Redo (Some n) -> sprintf "Redo %d" n - | Search_pat (kind, pat) -> +let pp_macro pp_term = function + | Abort _ -> "Abort" + | Check (_, term) -> sprintf "Check %s" (pp_term term) + | Redo (_, None) -> "Redo" + | Redo (_, Some n) -> sprintf "Redo %d" n + | Search_pat (_, kind, pat) -> sprintf "search %s \"%s\"" (pp_search_kind kind) pat - | Search_term (kind, term) -> + | Search_term (_, kind, term) -> sprintf "search %s %s" (pp_search_kind kind) (pp_term term) - | Inductive (params, types) -> + | Undo (_, None) -> "Undo" + | Undo (_, Some n) -> sprintf "Undo %d" n + | Print (_, name) -> sprintf "Print \"%s\"" name + | Quit _ -> "Quit" + +let pp_macro_ast = pp_macro pp_term_ast +let pp_macro_cic = pp_macro pp_term_cic + +let pp_alias = function + | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"" id uri + | Symbol_alias (symb, instance, desc) -> + sprintf "alias symbol \"%s\" (instance %d) = \"%s\"" + symb instance desc + | Number_alias (instance,desc) -> + sprintf "alias num (instance %d) = \"%s\"" instance desc + +let pp_command = function + | Qed _ -> "Qed" + | Set (_, name, value) -> sprintf "Set \"%s\" \"%s\"" name value + | Inductive (_, params, types) -> let pp_params = function | [] -> "" | params -> " " ^ String.concat " " (List.map - (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term typ)) + (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term_ast typ)) params) in let pp_constructors constructors = String.concat "\n" - (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term typ)) + (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term_ast typ)) constructors) in let pp_type (name, _, typ, constructors) = - sprintf "\nwith %s: %s \\def\n%s" name (pp_term typ) + sprintf "\nwith %s: %s \\def\n%s" name (pp_term_ast typ) (pp_constructors constructors) in (match types with @@ -146,37 +162,36 @@ let pp_command = function let fst_typ_pp = sprintf "%sinductive %s%s: %s \\def\n%s" (if inductive then "" else "co") name (pp_params params) - (pp_term typ) (pp_constructors constructors) + (pp_term_ast typ) (pp_constructors constructors) in fst_typ_pp ^ String.concat "" (List.map pp_type tl)) - | Theorem (flavour, name, typ, body) -> + | Theorem (_, flavour, name, typ, body) -> sprintf "%s %s: %s %s" (pp_flavour flavour) (match name with None -> "" | Some name -> name) - (pp_term typ) + (pp_term_ast typ) (match body with | None -> "" - | Some body -> "\\def " ^ pp_term body) - | Undo None -> "Undo" - | Undo (Some n) -> sprintf "Undo %d" n + | Some body -> "\\def " ^ pp_term_ast body) + | Coercion (_,_) -> "Coercion IMPLEMENT ME!!!!!" + | Alias (_,s) -> pp_alias s let rec pp_tactical = function - | LocatedTactical (loc, tac) -> pp_tactical tac - - | Tactic tac -> pp_tactic tac - | Command cmd -> pp_command cmd - - | Fail -> "fail" - | Do (count, tac) -> sprintf "do %d %s" count (pp_tactical tac) - | IdTac -> "id" - | Repeat tac -> "repeat " ^ pp_tactical tac - | Seq tacs -> pp_tacticals tacs - | Then (tac, tacs) -> sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals tacs) - | Tries tacs -> sprintf "tries [%s]" (pp_tacticals tacs) - | Try tac -> "try " ^ pp_tactical tac + | Tactic (_, tac) -> pp_tactic tac + + | Fail _ -> "fail" + | Do (_, count, tac) -> sprintf "do %d %s" count (pp_tactical tac) + | IdTac _ -> "id" + | Repeat (_, tac) -> "repeat " ^ pp_tactical tac + | Seq (_, tacs) -> pp_tacticals tacs + | Then (_, tac, tacs) -> + sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals tacs) + | Tries (_, tacs) -> sprintf "tries [%s]" (pp_tacticals tacs) + | Try (_, tac) -> "try " ^ pp_tactical tac and pp_tacticals tacs = String.concat (tactical_separator ^ " ") (List.map pp_tactical tacs) let pp_tactical tac = pp_tactical tac ^ tactical_terminator +let pp_tactic tac = pp_tactic tac ^ tactic_terminator diff --git a/helm/ocaml/cic_transformations/tacticAstPp.mli b/helm/ocaml/cic_transformations/tacticAstPp.mli index 356b07e76..f9fe2b2b8 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.mli +++ b/helm/ocaml/cic_transformations/tacticAstPp.mli @@ -24,6 +24,10 @@ *) val pp_tactic: (CicAst.term, string) TacticAst.tactic -> string - +val pp_command: CicAst.term TacticAst.command -> string +val pp_macro: ('a -> string) -> 'a TacticAst.macro -> string +val pp_macro_ast: CicAst.term TacticAst.macro -> string +val pp_macro_cic: Cic.term TacticAst.macro -> string val pp_tactical: (CicAst.term, string) TacticAst.tactical -> string +val pp_alias: TacticAst.alias_spec -> string diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index d18458e2b..b8784d717 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -83,7 +83,7 @@ let rec deref subst = Cic.Meta(n,l) as t -> (try deref subst - (CicSubstitution.lift_meta + (CicSubstitution.subst_meta l (third (CicUtil.lookup_subst n subst))) with CicUtil.Subst_not_found _ -> t) @@ -183,7 +183,7 @@ let apply_subst_gen ~appl_fun subst term = | C.Meta (i, l) -> (try let (_, t,_) = lookup_subst i subst in - um_aux (S.lift_meta l t) + um_aux (S.subst_meta l t) with CicUtil.Subst_not_found _ -> (* unconstrained variable, i.e. free in subst*) let l' = @@ -657,7 +657,7 @@ let delift n subst context metasenv l t = | C.Meta (i, l1) as t -> (try let (_,t,_) = CicUtil.lookup_subst i subst in - deliftaux k (CicSubstitution.lift_meta l1 t) + deliftaux k (CicSubstitution.subst_meta l1 t) with CicUtil.Subst_not_found _ -> (* see the top level invariant *) if (i = n) then diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 8401ad5ad..621834e33 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -224,17 +224,17 @@ and type_of_aux' metasenv context t ugraph = canonical_context l ugraph in (* trust or check ??? *) - C.Meta (n,l'),CicSubstitution.lift_meta l' ty, + C.Meta (n,l'),CicSubstitution.subst_meta l' ty, subst', metasenv', ugraph1 (* type_of_aux subst metasenv - context (CicSubstitution.lift_meta l term) *) + context (CicSubstitution.subst_meta l term) *) with CicUtil.Subst_not_found _ -> let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in let l',subst',metasenv', ugraph1 = check_metasenv_consistency n subst metasenv context canonical_context l ugraph in - C.Meta (n,l'),CicSubstitution.lift_meta l' ty, + C.Meta (n,l'),CicSubstitution.subst_meta l' ty, subst', metasenv',ugraph1) | C.Sort (C.Type tno) -> let tno' = CicUniv.fresh() in @@ -605,14 +605,14 @@ and type_of_aux' metasenv context t ugraph = function [] -> [] | (Some (n,C.Decl t))::tl -> - (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl) + (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl) | (Some (n,C.Def (t,None)))::tl -> - (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl) + (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl) | None::tl -> None::(aux (i+1) tl) | (Some (n,C.Def (t,Some ty)))::tl -> (Some (n, - C.Def ((S.lift_meta l (S.lift i t)), - Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl) + C.Def ((S.subst_meta l (S.lift i t)), + Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl) in aux 1 canonical_context in diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index e521c6570..130799ea4 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -65,7 +65,7 @@ let rec deref subst = Cic.Meta(n,l) as t -> (try deref subst - (CicSubstitution.lift_meta + (CicSubstitution.subst_meta l (snd (CicUtil.lookup_subst n subst))) with CicUtil.Subst_not_found _ -> t) @@ -99,7 +99,7 @@ let rec beta_expand test_equality_only metasenv subst context t arg ugraph = | C.Meta (i,l) as t-> (try let (_, t') = CicMetaSubst.lookup_subst i subst in - aux metasenv subst n context (CicSubstitution.lift_meta l t') + aux metasenv subst n context (CicSubstitution.subst_meta l t') ugraph with CicMetaSubst.SubstNotFound _ -> let (subst, metasenv, context, local_context,ugraph1) = @@ -417,7 +417,7 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str begin try let (_, oldt) = CicMetaSubst.lookup_subst n subst in - let lifted_oldt = S.lift_meta l oldt in + let lifted_oldt = S.subst_meta l oldt in let ty_lifted_oldt,ugraph1 = type_of_aux' metasenv subst context lifted_oldt ugraph in @@ -436,7 +436,7 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str let tyt,ugraph1 = type_of_aux' metasenv subst context t ugraph in fo_unif_subst test_equality_only - subst context metasenv tyt (S.lift_meta l meta_type) ugraph1 + subst context metasenv tyt (S.subst_meta l meta_type) ugraph1 with AssertFailure _ -> (* TODO huge hack!!!! * we keep on unifying/refining in the hope that the problem will be @@ -471,7 +471,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; (* Unifying the types may have already instantiated n. Let's check *) try let (_, oldt) = CicMetaSubst.lookup_subst n subst in - let lifted_oldt = S.lift_meta l oldt in + let lifted_oldt = S.subst_meta l oldt in fo_unif_subst_ordered test_equality_only subst context metasenv t lifted_oldt ugraph2 with @@ -495,7 +495,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; in fo_unif_subst test_equality_only - subst context metasenv tyt (S.lift_meta l meta_type) ugraph1 + subst context metasenv tyt (S.subst_meta l meta_type) ugraph1 with UnificationFailure msg | Uncertain msg -> @@ -532,7 +532,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; (* Unifying the types may have already instantiated n. Let's check *) try let (_, oldt,_) = CicUtil.lookup_subst n subst in - let lifted_oldt = S.lift_meta l oldt in + let lifted_oldt = S.subst_meta l oldt in fo_unif_subst_ordered test_equality_only subst context metasenv t lifted_oldt ugraph2 with @@ -634,7 +634,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; *) (try let (_,t,_) = CicUtil.lookup_subst i subst in - let lifted = S.lift_meta l t in + let lifted = S.subst_meta l t in let reduced = beta_reduce (Cic.Appl (lifted::args)) in fo_unif_subst test_equality_only @@ -649,7 +649,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; | _, C.Meta (i,l)::args when not(exists_a_meta args) -> (try let (_,t,_) = CicUtil.lookup_subst i subst in - let lifted = S.lift_meta l t in + let lifted = S.subst_meta l t in let reduced = beta_reduce (Cic.Appl (lifted::args)) in fo_unif_subst test_equality_only diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml index 712e8aae2..6aad3676d 100644 --- a/helm/ocaml/cic_unification/coercGraph.ml +++ b/helm/ocaml/cic_unification/coercGraph.ml @@ -25,11 +25,13 @@ open Printf;; +type coercions = (UriManager.uri * UriManager.uri * UriManager.uri) list + (* the list of known coercions (MUST be transitively closed) *) let coercions = ref [ (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)", UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con", - UriManager.uri_of_string "cic://Coq/Reals/Raxioms/INR.con") ; + UriManager.uri_of_string "cic:/Coq/Reals/Raxioms/INR.con") ; ( UriManager.uri_of_string "cic:/CoRN/algebra/CFields/CField.ind#xpointer(1/1)", diff --git a/helm/ocaml/cic_unification/coercGraph.mli b/helm/ocaml/cic_unification/coercGraph.mli index 9cbff65b9..cb0e51ca6 100644 --- a/helm/ocaml/cic_unification/coercGraph.mli +++ b/helm/ocaml/cic_unification/coercGraph.mli @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +type coercions = (UriManager.uri * UriManager.uri * UriManager.uri) list + val look_for_coercion : UriManager.uri -> UriManager.uri -> Cic.term option diff --git a/helm/ocaml/hbugs/Makefile b/helm/ocaml/hbugs/Makefile index af2d287ae..542bd2e3a 100644 --- a/helm/ocaml/hbugs/Makefile +++ b/helm/ocaml/hbugs/Makefile @@ -14,7 +14,7 @@ PACKAGE = hbugs REQUIRES = \ pcre lablgtk2.glade \ - helm-thread helm-xml helm-pxp helm-tactics + helm-thread helm-xml helm-pxp helm-tactics helm-registry IMPLEMENTATION_FILES = \ hbugs_misc.ml \ diff --git a/helm/ocaml/hbugs/broker.ml b/helm/ocaml/hbugs/broker.ml index 2ff8b9834..b86c08b9b 100644 --- a/helm/ocaml/hbugs/broker.ml +++ b/helm/ocaml/hbugs/broker.ml @@ -31,7 +31,6 @@ open Printf;; let debug = true ;; let debug_print s = if debug then prerr_endline s ;; -Http_common.debug := false;; let daemon_name = "H-Bugs Broker" ;; let default_port = 49081 ;; diff --git a/helm/ocaml/hbugs/hbugs_common.ml b/helm/ocaml/hbugs/hbugs_common.ml index 3b19ceec0..6e060de7a 100644 --- a/helm/ocaml/hbugs/hbugs_common.ml +++ b/helm/ocaml/hbugs/hbugs_common.ml @@ -30,17 +30,17 @@ open Hbugs_types;; open Printf;; let rec string_of_hint = function - | Use_ring_Luke -> "Use Ring, Luke!" - | Use_fourier_Luke -> "Use Fourier, Luke!" - | Use_reflexivity_Luke -> "Use reflexivity, Luke!" - | Use_symmetry_Luke -> "Use symmetry, Luke!" - | Use_assumption_Luke -> "Use assumption, Luke!" - | Use_contradiction_Luke -> "Use contradiction, Luke!" - | Use_exists_Luke -> "Use exists, Luke!" - | Use_split_Luke -> "Use split, Luke!" - | Use_left_Luke -> "Use left, Luke!" - | Use_right_Luke -> "Use right, Luke!" - | Use_apply_Luke term -> sprintf "Apply %s, Luke!" term + | Use_ring -> "Use Ring, Luke!" + | Use_fourier -> "Use Fourier, Luke!" + | Use_reflexivity -> "Use reflexivity, Luke!" + | Use_symmetry -> "Use symmetry, Luke!" + | Use_assumption -> "Use assumption, Luke!" + | Use_contradiction -> "Use contradiction, Luke!" + | Use_exists -> "Use exists, Luke!" + | Use_split -> "Use split, Luke!" + | Use_left -> "Use left, Luke!" + | Use_right -> "Use right, Luke!" + | Use_apply term -> sprintf "Apply %s, Luke!" term | Hints hints -> String.concat "; " (List.map string_of_hint hints) ;; diff --git a/helm/ocaml/hbugs/hbugs_messages.ml b/helm/ocaml/hbugs/hbugs_messages.ml index d792c3250..a6aa34b31 100644 --- a/helm/ocaml/hbugs/hbugs_messages.ml +++ b/helm/ocaml/hbugs/hbugs_messages.ml @@ -100,17 +100,17 @@ let parse_state (root: ('a node extension as 'a) node) = let parse_hint node = let rec parse_hint_node node = match node#node_type with - | T_element "ring" -> Use_ring_Luke - | T_element "fourier" -> Use_fourier_Luke - | T_element "reflexivity" -> Use_reflexivity_Luke - | T_element "symmetry" -> Use_symmetry_Luke - | T_element "assumption" -> Use_assumption_Luke - | T_element "contradiction" -> Use_contradiction_Luke - | T_element "exists" -> Use_exists_Luke - | T_element "split" -> Use_split_Luke - | T_element "left" -> Use_left_Luke - | T_element "right" -> Use_right_Luke - | T_element "apply" -> Use_apply_Luke node#data + | T_element "ring" -> Use_ring + | T_element "fourier" -> Use_fourier + | T_element "reflexivity" -> Use_reflexivity + | T_element "symmetry" -> Use_symmetry + | T_element "assumption" -> Use_assumption + | T_element "contradiction" -> Use_contradiction + | T_element "exists" -> Use_exists + | T_element "split" -> Use_split + | T_element "left" -> Use_left + | T_element "right" -> Use_right + | T_element "apply" -> Use_apply node#data | T_element "hints" -> Hints (List.map parse_hint_node (List.filter is_xml_element node#sub_nodes)) @@ -243,17 +243,17 @@ let pp_state = function | None -> "\n" let rec pp_hint = function - | Use_ring_Luke -> sprintf "" - | Use_fourier_Luke -> sprintf "" - | Use_reflexivity_Luke -> sprintf "" - | Use_symmetry_Luke -> sprintf "" - | Use_assumption_Luke -> sprintf "" - | Use_contradiction_Luke -> sprintf "" - | Use_exists_Luke -> sprintf "" - | Use_split_Luke -> sprintf "" - | Use_left_Luke -> sprintf "" - | Use_right_Luke -> sprintf "" - | Use_apply_Luke term -> sprintf "%s" term + | Use_ring -> sprintf "" + | Use_fourier -> sprintf "" + | Use_reflexivity -> sprintf "" + | Use_symmetry -> sprintf "" + | Use_assumption -> sprintf "" + | Use_contradiction -> sprintf "" + | Use_exists -> sprintf "" + | Use_split -> sprintf "" + | Use_left -> sprintf "" + | Use_right -> sprintf "" + | Use_apply term -> sprintf "%s" term | Hints hints -> sprintf "\n%s\n" (String.concat "\n" (List.map pp_hint hints)) diff --git a/helm/ocaml/hbugs/hbugs_types.mli b/helm/ocaml/hbugs/hbugs_types.mli index ebfa17994..e3067f2e9 100644 --- a/helm/ocaml/hbugs/hbugs_types.mli +++ b/helm/ocaml/hbugs/hbugs_types.mli @@ -37,17 +37,17 @@ type state = (* proof assitant's state: proof type, proof body, goal *) type hint = (* tactics usage related hints *) - | Use_ring_Luke - | Use_fourier_Luke - | Use_reflexivity_Luke - | Use_symmetry_Luke - | Use_assumption_Luke - | Use_contradiction_Luke - | Use_exists_Luke - | Use_split_Luke - | Use_left_Luke - | Use_right_Luke - | Use_apply_Luke of string (* use apply tactic on embedded term *) + | Use_ring + | Use_fourier + | Use_reflexivity + | Use_symmetry + | Use_assumption + | Use_contradiction + | Use_exists + | Use_split + | Use_left + | Use_right + | Use_apply of string (* use apply tactic on embedded term *) (* hints list *) | Hints of hint list diff --git a/helm/ocaml/hbugs/search_pattern_apply_tutor.ml b/helm/ocaml/hbugs/search_pattern_apply_tutor.ml index 0c1e7d0ae..1f5dad1bc 100644 --- a/helm/ocaml/hbugs/search_pattern_apply_tutor.ml +++ b/helm/ocaml/hbugs/search_pattern_apply_tutor.ml @@ -40,7 +40,7 @@ let slave mqi_handle (state, musing_id) = if uris = [] then Sorry else - Eureka (Hints (List.map (fun uri -> Use_apply_Luke uri) uris)) + Eureka (Hints (List.map (fun uri -> Use_apply uri) uris)) with Empty_must -> Sorry in let answer = Musing_completed (my_own_id, musing_id, hint) in diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml index 5ea64913d..0479264d4 100644 --- a/helm/ocaml/tactics/tacticals.ml +++ b/helm/ocaml/tactics/tacticals.ml @@ -47,7 +47,6 @@ let id_tac = in mk_tactic tac - (** naive implementation of ORELSE tactical, try a sequence of tactics in turn: if one fails pass to the next one and so on, eventually raises (failure "no @@ -110,9 +109,11 @@ let then_ ~start ~continuation = in mk_tactic (then_ ~start ~continuation) -(* Galla *) -(* si suppone che tutte le tattiche sollevino solamente Fail? *) - +let rec seq ~tactics = + match tactics with + | [] -> assert false + | [tac] -> tac + | hd :: tl -> then_ ~start:hd ~continuation:(seq ~tactics:tl) (* TODO: x debug: i due tatticali seguenti non contano quante volte hanno applicato la tattica *) @@ -187,6 +188,7 @@ let try_tactic ~tactic = mk_tactic (try_tactic ~tactic) ;; +let fail = mk_tactic (fun _ -> raise (Fail "fail tactical")) (* This tries tactics until one of them doesn't _solve_ the goal *) (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *) diff --git a/helm/ocaml/tactics/tacticals.mli b/helm/ocaml/tactics/tacticals.mli index 79a486acb..d7cc27545 100644 --- a/helm/ocaml/tactics/tacticals.mli +++ b/helm/ocaml/tactics/tacticals.mli @@ -38,6 +38,8 @@ val then_: start: ProofEngineTypes.tactic -> continuation: ProofEngineTypes.tactic -> ProofEngineTypes.tactic + (** "folding" of then_ *) +val seq: tactics: ProofEngineTypes.tactic list -> ProofEngineTypes.tactic val repeat_tactic: tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic @@ -52,7 +54,7 @@ val try_tactic: val solve_tactics: tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic - +val fail: ProofEngineTypes.tactic (* val prova_tac : ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/tactics.ml b/helm/ocaml/tactics/tactics.ml index 152e07b27..31364aa44 100644 --- a/helm/ocaml/tactics/tactics.ml +++ b/helm/ocaml/tactics/tactics.ml @@ -43,6 +43,7 @@ let exists = IntroductionTactics.exists_tac let fold = ReductionTactics.fold_tac let fourier = FourierR.fourier_tac let generalize = VariousTactics.generalize_tac +let set_goal = VariousTactics.set_goal let injection = DiscriminationTactics.injection_tac let intros = PrimitiveTactics.intros_tac let left = IntroductionTactics.left_tac diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index 7b771249e..d70c94ac5 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -32,6 +32,7 @@ val fourier : ProofEngineTypes.tactic val generalize : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term list -> ProofEngineTypes.tactic +val set_goal : int -> ProofEngineTypes.tactic val injection : term:Cic.term -> ProofEngineTypes.tactic val intros : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index be08c4d9e..c10060324 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -113,4 +113,12 @@ let generalize_tac PET.mk_tactic (generalize_tac mk_fresh_name_callback terms) ;; +let set_goal n = + ProofEngineTypes.mk_tactic + (fun (proof, goal) -> + let (_, metasenv, _, _) = proof in + if CicUtil.exists_meta n metasenv then + (proof, [n]) + else + raise (ProofEngineTypes.Fail ("no such meta: " ^ string_of_int n))) diff --git a/helm/ocaml/tactics/variousTactics.mli b/helm/ocaml/tactics/variousTactics.mli index d1da2fe98..eefdd9846 100644 --- a/helm/ocaml/tactics/variousTactics.mli +++ b/helm/ocaml/tactics/variousTactics.mli @@ -27,8 +27,11 @@ exception AllSelectedTermsMustBeConvertible;; val assumption_tac: ProofEngineTypes.tactic + val generalize_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term list -> ProofEngineTypes.tactic + (* change the current goal to those referred by the given meta number *) +val set_goal: int -> ProofEngineTypes.tactic diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml index 00cf4faa7..a4d260485 100644 --- a/helm/ocaml/urimanager/uriManager.ml +++ b/helm/ocaml/urimanager/uriManager.ml @@ -36,6 +36,7 @@ let eq uri1 uri2 = uri1 == uri2 ;; + let string_of_uri uri = match uri.(Array.length uri - 1) with | "" -> @@ -43,6 +44,8 @@ let string_of_uri uri = | _ -> String.concat "#" [ uri.(Array.length uri - 3); uri.(Array.length uri - 1) ] + + let name_of_uri uri = uri.(Array.length uri - 2);; let buri_of_uri uri = uri.(Array.length uri - 4);; let depth_of_uri uri = Array.length uri - 3;; @@ -179,3 +182,16 @@ let string_of_uriref (uri, fi) = | [t] -> str ^ xp t ^ ")" | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")" +let compare u1 u2 = + let su1 = string_of_uri u1 in + let su2 = string_of_uri u2 in + Pervasives.compare su1 su2 + +module OrderedUri = +struct + type t = uri + let compare = compare (* the one above, not Pervasives.compare *) +end + +module UriSet = Set.Make (OrderedUri) + diff --git a/helm/ocaml/urimanager/uriManager.mli b/helm/ocaml/urimanager/uriManager.mli index 12775af8d..771def7c1 100644 --- a/helm/ocaml/urimanager/uriManager.mli +++ b/helm/ocaml/urimanager/uriManager.mli @@ -28,6 +28,7 @@ exception IllFormedUri of string;; type uri val eq : uri -> uri -> bool +val compare : uri -> uri -> int val uri_of_string : string -> uri @@ -67,3 +68,5 @@ val mutconstruct: uri -> uri * int * int type uriref = uri * (int list) val string_of_uriref : uriref -> string +module UriSet: Set.S with type elt = uri + -- 2.39.2