X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Facic_procedural%2FproceduralConversion.ml;h=376313ac8f9de4577fbeae6780e57b33b6b77801;hb=24dd4569daf1d35bffaa813b8164058d8643f14d;hp=80aae9e7f3668b83fcee3378d7cb148174b5c31c;hpb=1dd6fc8c5d7bde039972a208c5eb03d3ea8303dd;p=helm.git

diff --git a/components/acic_procedural/proceduralConversion.ml b/components/acic_procedural/proceduralConversion.ml
index 80aae9e7f..376313ac8 100644
--- a/components/acic_procedural/proceduralConversion.ml
+++ b/components/acic_procedural/proceduralConversion.ml
@@ -30,6 +30,10 @@ module TC   = CicTypeChecker
 module D    = Deannotate
 module UM   = UriManager
 module Rd   = CicReduction
+module PEH  = ProofEngineHelpers
+module PT   = PrimitiveTactics
+
+module DTI  = DoubleTypeInference
 
 (* helpers ******************************************************************)
 
@@ -74,6 +78,46 @@ let lift k n =
    in
    lift_term k
 
+   let fake_annotate id c =
+      let get_binder c m =
+         try match List.nth c (pred m) with
+            | Some (C.Name s, _) -> s
+            | _ -> assert false
+         with
+            | Invalid_argument _ -> assert false
+      in
+      let mk_decl n v = Some (n, C.Decl v) in
+      let mk_def n v = Some (n, C.Def (v, None)) in
+      let mk_fix (name, _, _, bo) = mk_def (C.Name name) bo in
+      let mk_cofix (name, _, bo) = mk_def (C.Name name) bo in
+      let rec ann_xns c (uri, t) = uri, ann_term c t
+      and ann_ms c = function
+         | None -> None
+         | Some t -> Some (ann_term c t)
+      and ann_fix newc c (name, i, ty, bo) =
+         id, name, i, ann_term c ty, ann_term (List.rev_append newc c) bo
+      and ann_cofix newc c (name, ty, bo) =
+         id, name, ann_term c ty, ann_term (List.rev_append newc c) bo
+      and ann_term c = function
+         | C.Sort sort -> C.ASort (id, sort)
+         | C.Implicit ann -> C.AImplicit (id, ann)
+         | C.Rel m -> C.ARel (id, id, m, get_binder c m)
+         | C.Const (uri, xnss) -> C.AConst (id, uri, List.map (ann_xns c) xnss)
+         | C.Var (uri, xnss) -> C.AVar (id, uri, List.map (ann_xns c) xnss)
+         | C.MutInd (uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (ann_xns c) xnss)
+         | C.MutConstruct (uri, tyno, consno, xnss) -> C.AMutConstruct (id, uri,tyno,consno, List.map (ann_xns c) xnss)
+         | C.Meta (i, mss) -> C.AMeta(id, i, List.map (ann_ms c) mss)
+         | C.Appl ts -> C.AAppl (id, List.map (ann_term c) ts)
+         | C.Cast (te, ty) -> C.ACast (id, ann_term c te, ann_term c ty)
+         | C.MutCase (sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, ann_term c outty, ann_term c t, List.map (ann_term c) pl)
+         | C.Prod (n, s, t) -> C.AProd (id, n, ann_term c s, ann_term (mk_decl n s :: c) t)
+         | C.Lambda (n, s, t) -> C.ALambda (id, n, ann_term c s, ann_term (mk_decl n s :: c) t)
+         | C.LetIn (n, s, t) -> C.ALetIn (id, n, ann_term c s, ann_term (mk_def n s :: c) t)
+         | C.Fix (i, fl) -> C.AFix (id, i, List.map (ann_fix (List.rev_map mk_fix fl) c) fl)
+         | C.CoFix (i, fl) -> C.ACoFix (id, i, List.map (ann_cofix (List.rev_map mk_cofix fl) c) fl)
+      in
+      ann_term c
+
 let clear_absts m =
    let rec aux k n = function
       | C.AImplicit (_, None) as t         -> t
@@ -142,3 +186,66 @@ let generalize n =
 let mk_pattern psno predicate =
    let body = generalize psno predicate in
    clear_absts 0 psno body
+
+let get_clears c p xtypes = 
+   let meta = C.Implicit None in
+   let rec aux c names p it et = function
+      | []                                                -> 
+         List.rev c, List.rev names         
+      | Some (C.Name name as n, C.Decl v) as hd :: tl     ->
+         let hd, names, v = 
+	    if DTI.does_not_occur 1 p && DTI.does_not_occur 1 it && DTI.does_not_occur 1 et then 
+	       Some (C.Anonymous, C.Decl v), name :: names, meta 
+	    else 
+	       hd, names, v
+	 in
+	 let p = C.Lambda (n, v, p) in
+	 let it = C.Prod (n, v, it) in
+	 let et = C.Prod (n, v, et) in
+	 aux (hd :: c) names p it et tl
+      | Some (C.Name name as n, C.Def (v, x)) as hd :: tl ->
+         let hd, names, v = 
+	    if DTI.does_not_occur 1 p && DTI.does_not_occur 1 it && DTI.does_not_occur 1 et then 
+	       Some (C.Anonymous, C.Def (v, x)), name :: names, meta
+	    else 
+	       hd, names, v
+	 in
+	 let p = C.LetIn (n, v, p) in
+	 let it = C.LetIn (n, v, it) in
+	 let et = C.LetIn (n, v, et) in
+	 aux (hd :: c) names p it et tl
+      | Some (C.Anonymous as n, C.Decl v) as hd :: tl     ->
+	 let p = C.Lambda (n, meta, p) in
+	 let it = C.Lambda (n, meta, it) in
+	 let et = C.Lambda (n, meta, et) in
+	 aux (hd :: c) names p it et tl
+      | Some (C.Anonymous as n, C.Def (v, _)) as hd :: tl ->
+	 let p = C.LetIn (n, meta, p) in
+	 let it = C.LetIn (n, meta, it) in
+	 let et = C.LetIn (n, meta, et) in
+	 aux (hd :: c) names p it et tl
+      | None :: tl                                        -> assert false
+   in
+   match xtypes with 
+      | Some (it, et) -> aux [] [] p it et c
+      | None          -> c, []
+
+let clear c hyp =
+   let rec aux c = function
+      | []            -> List.rev c
+      | Some (C.Name name, entry) :: tail when name = hyp ->
+	 aux (Some (C.Anonymous, entry) :: c) tail
+      | entry :: tail -> aux (entry :: c) tail
+   in
+   aux [] c
+
+let elim_inferred_type context goal arg using cpattern =
+   let metasenv, ugraph = [], Un.empty_ugraph in 
+   let ety, _ugraph = TC.type_of_aux' metasenv context using ugraph in
+   let _splits, args_no = PEH.split_with_whd (context, ety) in
+   let _metasenv, predicate, _arg, actual_args = PT.mk_predicate_for_elim 
+      ~context ~metasenv ~ugraph ~goal ~arg ~using ~cpattern ~args_no
+   in
+   let ty = C.Appl (predicate :: actual_args) in
+   let upto = List.length actual_args in
+   Rd.head_beta_reduce ~delta:false ~upto ty