diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-05-29 10:48:37 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-05-29 10:48:37 +0000 |
| commit | 32170384190168856efeac5bcf90edf1170b54d6 (patch) | |
| tree | 0ea86b672df93d997fa1cab70b678ea7abdcf171 /tactics/hipattern.ml | |
| parent | 1e5182e9d5c29ae9adeed20dae32969785758809 (diff) | |
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/hipattern.ml')
| -rw-r--r-- | tactics/hipattern.ml | 21 |
1 files changed, 18 insertions, 3 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 39c2bd8f7..8e7648704 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -125,6 +125,17 @@ let is_unit_type t = op2bool (match_with_unit_type t) inductive binary relation R, so that R has only one constructor establishing its reflexivity. *) +(* ["(A : ?)(x:A)(? A x x)"] and ["(x : ?)(? x x)"] *) +let x = Name (id_of_string "x") +let y = Name (id_of_string "y") +let name_A = Name (id_of_string "A") +let coq_refl_rel1_pattern = + PProd + (name_A, PMeta None, + PProd (x, PRel 1, PApp (PMeta None, [|PRel 2; PRel 1; PRel 1|]))) +let coq_refl_rel2_pattern = + PProd (x, PMeta None, PApp (PMeta None, [|PRel 1; PRel 1|])) + let match_with_equation t = let (hdapp,args) = decompose_app t in match (kind_of_term hdapp) with @@ -133,8 +144,8 @@ let match_with_equation t = let constr_types = mip.mind_nf_lc in let nconstr = Array.length mip.mind_consnames in if nconstr = 1 && - (is_matching (build_coq_refl_rel1_pattern ()) constr_types.(0) || - is_matching (build_coq_refl_rel1_pattern ()) constr_types.(0)) + (is_matching coq_refl_rel1_pattern constr_types.(0) || + is_matching coq_refl_rel1_pattern constr_types.(0)) then Some (hdapp,args) else @@ -143,9 +154,13 @@ let match_with_equation t = let is_equation t = op2bool (match_with_equation t) +(* ["(?1 -> ?2)"] *) +let imp a b = PProd (Anonymous, a, b) +let coq_arrow_pattern = imp (PMeta (Some 1)) (PMeta (Some 2)) + let match_with_nottype t = try - match matches (build_coq_arrow_pattern ()) t with + match matches coq_arrow_pattern t with | [(1,arg);(2,mind)] -> if is_empty_type mind then Some (mind,arg) else None | _ -> anomaly "Incorrect pattern matching" |