- new devel contribs/LAMBDA-TYPES/Base-2 with the automatically generated

[helm.git] / components / acic_procedural / proceduralConversion.ml

diff --git a/components/acic_procedural/proceduralConversion.ml b/components/acic_procedural/proceduralConversion.ml
index b8cdc08ea1b3af2a0288ef6239f3718ad4aed5ea..376313ac8f9de4577fbeae6780e57b33b6b77801 100644 (file)
--- a/components/acic_procedural/proceduralConversion.ml
+++ b/components/acic_procedural/proceduralConversion.ml
@@ -30,6 +30,8 @@ module TC   = CicTypeChecker
 module D    = Deannotate
 module UM   = UriManager
 module Rd   = CicReduction
+module PEH  = ProofEngineHelpers
+module PT   = PrimitiveTactics
 
 module DTI  = DoubleTypeInference
 
@@ -76,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
@@ -196,3 +238,14 @@ let clear c hyp =
       | 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