paths trough terms implemented with a nice hack :)

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index 54bd178a0bed18232d5f153a5e82718d10cb73c3..5a64429a388da80c174e5ca3bfbce28a451f5ad5 100644 (file)
--- 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 733166d7eeb0dacf27f587db1c136fc57ca2fd61..6bdbd8057015a58cc7bd119ff38dc5fc463aa849 100644 (file)
--- 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 238eb93673f6f46830c3f6784d32e187f479e0fb..6e368d79bdbb13fd0ab4fbf7171fa765c96a057c 100644 (file)
--- 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 4f8f8e78a43a1c9bd34028fc3b5f5b6efe363377..b71e908856ba017df051a5d244f7ab39a1fd9035 100644 (file)
--- 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 ac9b977927bb9c69a86c64198949fba1cadb4ab8..b659b38ffac13a4828ac69c8bc76364740d1c39f 100644 (file)
--- 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 6bb67af227b5c96edb87ea3ea873bd5ece63dd81..89f8907fa32fe45648996bffc44146697a147a11 100644 (file)
--- 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 52506019e4b92790e2fdd6290576bd838ba1a9cd..7fabafda3e5f1707172048a54e7e327d7a3984e7 100644 (file)
--- 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 cb06a8edf6dc9d67f410fed7689a6bf6ad2e8230..d2df977fa68dfd72c5c9484c7a1e8bd6fbb90f8a 100644 (file)
--- 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 a4ec56deecfc3218e69d364211cbce59c7119539..9882aa0e92b0335f0aef7467116c87e5c14e9c0a 100644 (file)
--- 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 d356499a1d50fccad761e5c7ed7d3adb8d2ae6f6..d3d36ca6e9cf630cfd64e93ea07e732a8df3973f 100644 (file)
--- 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 f97b4cf63903674b15836112f72b8d4cd868b856..e1b3f9107493fcb4ea4a47b1b88efcde4b4f987a 100644 (file)
--- 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 d1441aa4b37b89f6c641ca2e6832e69fd731e93f..3ac33d2f58d99a10e5d3cf84b05e6cdf78e1ad02 100644 (file)
--- 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 b69e43e88328ebcec45200a7303ecc0686e7d742..a91985290838195bfcd4a9813a0d5de8b5c674a9 100644 (file)
--- 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