From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 1 Jun 2005 14:34:36 +0000 (+0000)
Subject: paths trough terms implemented with a nice hack :)
X-Git-Tag: PRE_INDEX_1~77
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aeec9dd128be72caf5a39bac3a0ef34b564ecd8b;p=helm.git

paths trough terms implemented with a nice hack :)
---

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