From aeec9dd128be72caf5a39bac3a0ef34b564ecd8b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 1 Jun 2005 14:34:36 +0000 Subject: [PATCH] paths trough terms implemented with a nice hack :) --- helm/ocaml/cic/cicUtil.ml | 1 + helm/ocaml/cic_disambiguation/cicTextualLexer2.ml | 2 ++ helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 6 +++++- helm/ocaml/cic_disambiguation/disambiguate.ml | 3 ++- helm/ocaml/cic_disambiguation/disambiguate.mli | 5 +++++ helm/ocaml/cic_transformations/cicAst.mli | 1 - helm/ocaml/cic_transformations/tacticAst.ml | 3 ++- helm/ocaml/cic_transformations/tacticAst2Box.ml | 1 + helm/ocaml/cic_transformations/tacticAstPp.ml | 1 + helm/ocaml/tactics/reductionTactics.ml | 4 ++++ helm/ocaml/tactics/reductionTactics.mli | 3 +++ helm/ocaml/tactics/tactics.ml | 2 +- helm/ocaml/tactics/tactics.mli | 3 +++ 13 files changed, 30 insertions(+), 5 deletions(-) diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index 54bd178a0..5a64429a3 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -175,6 +175,7 @@ let select ~term ~context = let rec aux context term = match (context, term) with | Cic.Implicit (Some `Hole), t -> [t] + | Cic.Implicit None,_ -> [] | Cic.Meta (_, ctxt1), Cic.Meta (_, ctxt2) -> List.concat (List.map2 diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml index 733166d7e..6bdbd8057 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml @@ -32,6 +32,7 @@ let regexp digit = [ '0' - '9' ] let regexp blank = [ ' ' '\t' '\n' ] let regexp paren = [ '(' '[' '{' ')' ']' '}' ] let regexp implicit = '?' +let regexp placeholder = '%' let regexp symbol_char = [^ 'a' - 'z' 'A' - 'Z' '0' - '9' ' ' '\t' '\n' @@ -127,6 +128,7 @@ let rec token comments = lexer | paren -> return lexbuf ("PAREN", Ulexing.utf8_lexeme lexbuf) | meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf) | implicit -> return lexbuf ("IMPLICIT", Ulexing.utf8_lexeme lexbuf) + | placeholder -> return lexbuf ("PLACEHOLDER", Ulexing.utf8_lexeme lexbuf) | qstring -> return lexbuf ("QSTRING", remove_quotes (Ulexing.utf8_lexeme lexbuf)) | symbol -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 238eb9367..6e368d79b 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -279,6 +279,7 @@ EXTEND | n = substituted_name -> return_term loc n | i = NUM -> return_term loc (CicAst.Num (i, (fresh_num_instance ()))) | IMPLICIT -> return_term loc CicAst.Implicit + | PLACEHOLDER -> return_term loc CicAst.UserInput | m = META; substs = [ PAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; PAREN "]" -> @@ -322,7 +323,8 @@ EXTEND reduction_kind: [ [ [ IDENT "reduce" ] -> `Reduce | [ IDENT "simplify" ] -> `Simpl - | [ IDENT "whd" ] -> `Whd ] + | [ IDENT "whd" ] -> `Whd + | [ IDENT "normalize" ] -> `Normalize ] ]; tactic: [ [ [ IDENT "absurd" ]; t = tactic_term -> @@ -389,6 +391,8 @@ EXTEND | None, terms -> TacticAst.Reduce (loc, kind, Some (terms, `Goal)) | Some pat, [] -> fail loc "Missing term [list]" | Some pat, terms -> TacticAst.Reduce (loc, kind, Some (terms, pat))) + | kind = reduction_kind; where = IDENT ; IDENT "at" ; pat = term -> + TacticAst.ReduceAt (loc, kind, where, pat) | [ IDENT "reflexivity" ] -> TacticAst.Reflexivity loc | [ IDENT "replace" ]; diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 4f8f8e78a..b71e90885 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -265,6 +265,8 @@ let interpretate ~context ~env ast = CicEnvironment.CircularDependency _ -> raise DisambiguateChoices.Invalid_choice)) | CicAst.Implicit -> Cic.Implicit None + | CicAst.UserInput -> Cic.Implicit (Some `Hole) +(* | CicAst.UserInput -> assert false*) | CicAst.Num (num, i) -> resolve env (Num i) ~num () | CicAst.Meta (index, subst) -> let cic_subst = @@ -279,7 +281,6 @@ let interpretate ~context ~env ast = | CicAst.Sort `CProp -> Cic.Sort Cic.CProp | CicAst.Symbol (symbol, instance) -> resolve env (Symbol (symbol, instance)) () - | CicAst.UserInput -> assert false and aux_option loc context = function | None -> Cic.Implicit (Some `Type) | Some term -> aux loc context term diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index ac9b97792..b659b38ff 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -29,6 +29,11 @@ open DisambiguateTypes exception NoWellTypedInterpretation +val interpretate: + context:Cic.name list -> + env:DisambiguateTypes.environment -> + CicAst.term -> Cic.term + module type Disambiguator = sig val disambiguate_term : diff --git a/helm/ocaml/cic_transformations/cicAst.mli b/helm/ocaml/cic_transformations/cicAst.mli index 6bb67af22..89f8907fa 100644 --- a/helm/ocaml/cic_transformations/cicAst.mli +++ b/helm/ocaml/cic_transformations/cicAst.mli @@ -51,7 +51,6 @@ type term_attribute = type term = | AttributedTerm of term_attribute * term - | Appl of term list | Binder of binder_kind * capture_variable * term (* kind, name, body *) | Case of term * string option * term option * (case_pattern * term) list diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 52506019e..7fabafda3 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -24,7 +24,7 @@ *) type direction = [ `Left | `Right ] -type reduction_kind = [ `Reduce | `Simpl | `Whd ] +type reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ] (* type 'term pattern = Pattern of 'term *) (* everywhere includes goal and hypotheses *) @@ -60,6 +60,7 @@ type ('term, 'ident) tactic = | 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 *) *) + | ReduceAt of loc * reduction_kind * 'ident * 'term | 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, diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml index cb06a8edf..d2df977fa 100644 --- a/helm/ocaml/cic_transformations/tacticAst2Box.ml +++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml @@ -106,6 +106,7 @@ let string_of_kind = function | `Reduce -> "reduce" | `Simpl -> "simplify" | `Whd -> "whd" + | `Normalize -> "normalize" let dummy_tbl = Hashtbl.create 0 diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index a4ec56dee..9882aa0e9 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -41,6 +41,7 @@ let pp_reduction_kind = function | `Reduce -> "reduce" | `Simpl -> "simplify" | `Whd -> "whd" + | `Normalize -> "normalize" let rec pp_tactic = function | Absurd (_, term) -> "absurd" ^ pp_term_ast term diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml index d356499a1..d3d36ca6e 100644 --- a/helm/ocaml/tactics/reductionTactics.ml +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -103,6 +103,10 @@ let whd_tac ~also_in_hypotheses ~terms = mk_tactic ( reduction_tac ~reduction:CicReduction.whd ~also_in_hypotheses ~terms);; +let normalize_tac ~also_in_hypotheses ~terms = + mk_tactic ( reduction_tac ~reduction:CicReduction.normalize + ~also_in_hypotheses ~terms);; + let fold_tac ~reduction ~also_in_hypotheses ~term = let fold_tac ~reduction ~also_in_hypotheses ~term (proof,goal) = let curi,metasenv,pbo,pty = proof in diff --git a/helm/ocaml/tactics/reductionTactics.mli b/helm/ocaml/tactics/reductionTactics.mli index f97b4cf63..e1b3f9107 100644 --- a/helm/ocaml/tactics/reductionTactics.mli +++ b/helm/ocaml/tactics/reductionTactics.mli @@ -33,6 +33,9 @@ val reduce_tac: val whd_tac: also_in_hypotheses:bool -> terms:(Cic.term list option) -> ProofEngineTypes.tactic +val normalize_tac: + also_in_hypotheses:bool -> terms:(Cic.term list option) -> + ProofEngineTypes.tactic val fold_tac: reduction:(Cic.context -> Cic.term -> Cic.term) -> diff --git a/helm/ocaml/tactics/tactics.ml b/helm/ocaml/tactics/tactics.ml index d1441aa4b..3ac33d2f5 100644 --- a/helm/ocaml/tactics/tactics.ml +++ b/helm/ocaml/tactics/tactics.ml @@ -63,4 +63,4 @@ let split = IntroductionTactics.split_tac let symmetry = EqualityTactics.symmetry_tac let transitivity = EqualityTactics.transitivity_tac let whd = ReductionTactics.whd_tac - +let normalize = ReductionTactics.normalize_tac diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index b69e43e88..a91985290 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -63,3 +63,6 @@ val transitivity : term:Cic.term -> ProofEngineTypes.tactic val whd : also_in_hypotheses:bool -> terms:Cic.term list option -> ProofEngineTypes.tactic +val normalize : + also_in_hypotheses:bool -> + terms:Cic.term list option -> ProofEngineTypes.tactic -- 2.39.2