Very experimental commit: the type of the source is now required in LetIns

[helm.git] / helm / software / components / acic_content / termAcicContent.ml

diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml
index 9a30b50fb6ef1b2618171c38f74ebc490e52e1da..f3806beea63896e2a3217df528a8806649328832 100644 (file)
--- a/helm/software/components/acic_content/termAcicContent.ml
+++ b/helm/software/components/acic_content/termAcicContent.ml
@@ -70,7 +70,7 @@ let constructor_of_inductive_type uri i j =
 let left_params_no_of_inductive_type uri =
    snd (get_types uri)
 
-let ast_of_acic0 term_info acic k =
+let ast_of_acic0 ~output_type term_info acic k =
   let k = k term_info in
   let id_to_uris = term_info.uri in
   let register_uri id uri = Hashtbl.add id_to_uris id uri in
@@ -118,8 +118,8 @@ let ast_of_acic0 term_info acic k =
     | Cic.ALambda (id,n,s,t) ->
         idref id (Ast.Binder (`Lambda,
           (CicNotationUtil.name_of_cic_name n, Some (k s)), k t))
-    | Cic.ALetIn (id,n,s,t) ->
-        idref id (Ast.LetIn ((CicNotationUtil.name_of_cic_name n, None),
+    | Cic.ALetIn (id,n,s,ty,t) ->
+        idref id (Ast.LetIn ((CicNotationUtil.name_of_cic_name n, Some (k ty)),
           k s, k t))
     | Cic.AAppl (aid,(Cic.AConst _ as he::tl as args))
     | Cic.AAppl (aid,(Cic.AMutInd _ as he::tl as args))
@@ -196,12 +196,21 @@ let ast_of_acic0 term_info acic k =
             List.map2
               (fun (name, ty) pat ->
                 incr j;
-                let (capture_variables, rhs) = eat_branch lpsno ty pat in
-                ((name, Some (ctor_puri !j), capture_variables), rhs))
-              constructors patterns
+                let name,(capture_variables,rhs) =
+                 match output_type with
+                    `Term -> name, eat_branch lpsno ty pat
+                  | `Pattern -> "_", ([], k pat)
+                in
+                 Ast.Pattern (name, Some (ctor_puri !j), capture_variables), rhs
+              ) constructors patterns
           with Invalid_argument _ -> assert false
         in
-        idref id (Ast.Case (k te, Some case_indty, Some (k ty), patterns))
+        let indty =
+         match output_type with
+            `Pattern -> None
+          | `Term -> Some case_indty
+        in
+        idref id (Ast.Case (k te, indty, Some (k ty), patterns))
     | Cic.AFix (id, no, funs) -> 
         let defs = 
           List.map
@@ -323,11 +332,12 @@ let instantiate32 term_info idrefs env symbol args =
   if args = [] then head
   else Ast.Appl (head :: List.map instantiate_arg args)
 
-let rec ast_of_acic1 term_info annterm = 
+let rec ast_of_acic1 ~output_type term_info annterm = 
   let id_to_uris = term_info.uri in
   let register_uri id uri = Hashtbl.add id_to_uris id uri in
   match (get_compiled32 ()) annterm with
-  | None -> ast_of_acic0 term_info annterm ast_of_acic1
+  | None ->
+     ast_of_acic0 ~output_type term_info annterm (ast_of_acic1 ~output_type)
   | Some (env, ctors, pid) -> 
       let idrefs =
         List.map
@@ -341,7 +351,8 @@ let rec ast_of_acic1 term_info annterm =
           ctors
       in
       let env' =
-        List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) env
+       List.map
+        (fun (name, term) -> name, ast_of_acic1 ~output_type term_info term) env
       in
       let _, symbol, args, _ =
         try
@@ -357,16 +368,17 @@ let load_patterns32 t =
   in
   set_compiled32 (lazy (Acic2astMatcher.Matcher32.compiler t))
 
-let ast_of_acic id_to_sort annterm =
+let ast_of_acic ~output_type id_to_sort annterm =
   debug_print (lazy ("ast_of_acic <- "
     ^ CicPp.ppterm (Deannotate.deannotate_term annterm)));
   let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
-  let ast = ast_of_acic1 term_info annterm in
+  let ast = ast_of_acic1 ~output_type term_info annterm in
   debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast));
   ast, term_info.uri
 
+let counter = ref ~-1 
+let reset () = counter := ~-1;;
 let fresh_id =
-  let counter = ref ~-1 in
   fun () ->
     incr counter;
     !counter