first (almost) working version: apparently, only generation of coinductive

eliminators does not typecheck

diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml
index fb64aae09f00c3ff5437de495f03b69bde458d24..b46aa0b226516bcc8abab2bb9be679ef3583c435 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicElim.ml
+++ b/helm/ocaml/cic_proof_checking/cicElim.ml
@@ -37,19 +37,18 @@ let fresh_binder =
     | _ -> Cic.Anonymous
 
   (** verifies if a given inductive type occurs in a term in target position *)
-let rec recursive uri typeno subst = function
-  | Cic.Prod (_, _, target) -> recursive uri typeno subst target
-  | Cic.MutInd (uri', typeno', subst')
-  | Cic.Appl (Cic.MutInd  (uri', typeno', subst') :: _) ->
-      UriManager.eq uri uri' && typeno = typeno' && subst = subst'
-(*   | Cic.Appl args -> List.exists (recursive uri typeno subst) args *)
+let rec recursive uri typeno = function
+  | Cic.Prod (_, _, target) -> recursive uri typeno target
+  | Cic.MutInd (uri', typeno', [])
+  | Cic.Appl (Cic.MutInd  (uri', typeno', []) :: _) ->
+      UriManager.eq uri uri' && typeno = typeno'
   | _ -> false
 
   (** given a list of constructor types, return true if at least one of them is
   * recursive, false otherwise *)
-let recursive_type uri typeno subst constructors =
+let recursive_type uri typeno constructors =
   let rec aux = function
-    | Cic.Prod (_, src, tgt) -> recursive uri typeno subst src || aux tgt
+    | Cic.Prod (_, src, tgt) -> recursive uri typeno src || aux tgt
     | _ -> false
   in
   List.exists (fun (_, ty) -> aux ty) constructors
@@ -68,11 +67,10 @@ let rec split l n =
   * @param paramsno number of Prod to ignore in this constructor (i.e. number of
   * inductive parameters)
   * @param dependent true if we are in the dependent case (i.e. sort <> Prop) *)
-let rec delta (uri, typeno, subst) dependent paramsno consno t p args =
-  assert (subst = []);
+let rec delta (uri, typeno) dependent paramsno consno t p args =
   match t with
-  | Cic.MutInd (uri', typeno', subst') when
-    UriManager.eq uri uri' && typeno = typeno' && subst = subst' ->
+  | Cic.MutInd (uri', typeno', []) when
+    UriManager.eq uri uri' && typeno = typeno' ->
       if dependent then
         (match args with
         | [] -> assert false
@@ -80,8 +78,8 @@ let rec delta (uri, typeno, subst) dependent paramsno consno t p args =
         | _ -> unfold_appl (Cic.Appl [p; unfold_appl (Cic.Appl args)]))
       else
         p
-  | Cic.Appl (Cic.MutInd (uri', typeno', subst') :: tl) when
-    UriManager.eq uri uri' && typeno = typeno' && subst = subst' ->
+  | Cic.Appl (Cic.MutInd (uri', typeno', []) :: tl) when
+    UriManager.eq uri uri' && typeno = typeno' ->
       let (lparams, rparams) = split tl paramsno in
       if dependent then
         (match args with
@@ -95,22 +93,22 @@ let rec delta (uri, typeno, subst) dependent paramsno consno t p args =
         | [] -> p
         | _ -> Cic.Appl (p :: rparams))
   | Cic.Prod (binder, src, tgt) ->
-      if recursive uri typeno subst src then
+      if recursive uri typeno src then
         let args = List.map (CicSubstitution.lift 2) args in
         let phi =
           let src = CicSubstitution.lift 1 src in
-          delta (uri, typeno, subst) dependent paramsno consno src
+          delta (uri, typeno) dependent paramsno consno src
             (CicSubstitution.lift 1 p) [Cic.Rel 1]
         in
         let tgt = CicSubstitution.lift 1 tgt in
         Cic.Prod (fresh_binder dependent, src,
           Cic.Prod (Cic.Anonymous, phi,
-            delta (uri, typeno, subst) dependent paramsno consno tgt
+            delta (uri, typeno) dependent paramsno consno tgt
               (CicSubstitution.lift 2 p) (args @ [Cic.Rel 2])))
       else  (* non recursive *)
         let args = List.map (CicSubstitution.lift 1) args in
         Cic.Prod (fresh_binder dependent, src,
-          delta (uri, typeno, subst) dependent paramsno consno tgt
+          delta (uri, typeno) dependent paramsno consno tgt
             (CicSubstitution.lift 1 p) (args @ [Cic.Rel 1]))
   | _ -> assert false
 
@@ -126,9 +124,9 @@ let rec strip_left_params consno leftno = function
         strip_left_params consno (leftno - 1) tgt
   | _ -> assert false
 
-let delta (ury, typeno, subst) dependent paramsno consno t p args =
+let delta (ury, typeno) dependent paramsno consno t p args =
   let t = strip_left_params consno paramsno t in
-  delta (ury, typeno, subst) dependent paramsno consno t p args
+  delta (ury, typeno) dependent paramsno consno t p args
 
 let rec add_params binder indno ty eliminator =
   if indno = 0 then
@@ -164,7 +162,7 @@ let rec type_of_p sort dependent leftno indty = function
 let rec add_right_pi dependent strip liftno liftfrom rightno indty = function
   | Cic.Prod (_, src, tgt) when strip = 0 ->
       Cic.Prod (fresh_binder true,
-        CicSubstitution.lift_from (liftfrom + 1) liftno src,
+        CicSubstitution.lift_from liftfrom liftno src,
         add_right_pi dependent strip liftno (liftfrom + 1) rightno indty tgt)
   | Cic.Prod (_, _, tgt) ->
       add_right_pi dependent (strip - 1) liftno liftfrom rightno indty tgt
@@ -185,7 +183,7 @@ let rec add_right_lambda dependent strip liftno liftfrom rightno indty case =
 function
   | Cic.Prod (_, src, tgt) when strip = 0 ->
       Cic.Lambda (fresh_binder true,
-        CicSubstitution.lift_from (liftfrom + 1) liftno src,
+        CicSubstitution.lift_from liftfrom liftno src,
         add_right_lambda dependent strip liftno (liftfrom + 1) rightno indty
           case tgt)
   | Cic.Prod (_, _, tgt) ->
@@ -201,51 +199,55 @@ let string_of_sort = function
   | Cic.Set -> "Set"
   | Cic.Type _ -> "Type"
 
-let rec branch (uri, typeno, subst) insource paramsno t fix head args =
-  assert (subst = []);
+let rec branch (uri, typeno) insource paramsno t fix head args =
   match t with
-  | Cic.MutInd (uri', typeno', subst') when
-    UriManager.eq uri uri' && typeno = typeno' && subst = subst' ->
-      let head = if insource then fix else head in
-      (match args with
-      | [] -> head
-      | _ -> Cic.Appl (head :: args))
-  | Cic.Appl (Cic.MutInd (uri', typeno', subst') :: tl) when
-    UriManager.eq uri uri' && typeno = typeno' && subst = subst' ->
+  | Cic.MutInd (uri', typeno', []) when
+    UriManager.eq uri uri' && typeno = typeno' ->
+      if insource then
+        (match args with
+        | [arg] -> Cic.Appl (fix :: args)
+        | _ -> Cic.Appl (head :: [Cic.Appl args]))
+      else
+        (match args with
+        | [] -> head
+        | _ -> Cic.Appl (head :: args))
+  | Cic.Appl (Cic.MutInd (uri', typeno', []) :: tl) when
+    UriManager.eq uri uri' && typeno = typeno' ->
       if insource then
         let (lparams, rparams) = split tl paramsno in
-        Cic.Appl (fix :: rparams @ args)
+        match args with
+        | [arg] -> Cic.Appl (fix :: rparams @ args)
+        | _ -> Cic.Appl (fix :: rparams @ [Cic.Appl args])
       else
         (match args with
         | [] -> head
         | _ -> Cic.Appl (head :: args))
   | Cic.Prod (binder, src, tgt) ->
-      if recursive uri typeno subst src then
+      if recursive uri typeno src then
         let args = List.map (CicSubstitution.lift 1) args in
         let phi =
           let fix = CicSubstitution.lift 1 fix in
           let src = CicSubstitution.lift 1 src in
-          branch (uri, typeno, subst) true paramsno src fix head [Cic.Rel 1]
+          branch (uri, typeno) true paramsno src fix head [Cic.Rel 1]
         in
         Cic.Lambda (fresh_binder true, src,
-          branch (uri, typeno, subst) insource paramsno tgt
+          branch (uri, typeno) insource paramsno tgt
             (CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head)
             (args @ [Cic.Rel 1; phi]))
       else  (* non recursive *)
         let args = List.map (CicSubstitution.lift 1) args in
         Cic.Lambda (fresh_binder true, src,
-          branch (uri, typeno, subst) insource paramsno tgt
+          branch (uri, typeno) insource paramsno tgt
           (CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head)
             (args @ [Cic.Rel 1]))
   | _ -> assert false
 
-let branch (uri, typeno, subst) insource liftno paramsno t fix head args =
+let branch (uri, typeno) insource liftno paramsno t fix head args =
   let t = strip_left_params liftno paramsno t in
-  branch (uri, typeno, subst) insource paramsno t fix head args
+  branch (uri, typeno) insource paramsno t fix head args
 
 let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
   let (obj, univ) = (CicEnvironment.get_obj uri CicUniv.empty_ugraph) in
-  let subst = [] in
   match obj with
   | Cic.InductiveDefinition (indTypes, params, leftno) ->
       let (name, inductive, ty, constructors) =
@@ -261,14 +263,14 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
       if (not dependent) && (sort <> Cic.Prop) && (conslen > 1) then
         raise Can_t_eliminate;
       let indty =
-        let indty = Cic.MutInd (uri, typeno, subst) in
+        let indty = Cic.MutInd (uri, typeno, []) in
         if paramsno = 0 then
           indty
         else
           Cic.Appl (indty :: mk_rels 0 paramsno)
       in
       let mk_constructor consno =
-        let constructor = Cic.MutConstruct (uri, typeno, consno, subst) in
+        let constructor = Cic.MutConstruct (uri, typeno, consno, []) in
         if leftno = 0 then
           constructor
         else
@@ -286,7 +288,7 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
                 decr consno;
                 let p = Cic.Rel !consno in
                 Cic.Prod (Cic.Anonymous,
-                  (delta (uri, typeno, subst) dependent leftno !consno
+                  (delta (uri, typeno) dependent leftno !consno
                     constructor p [mk_constructor !consno]),
                   acc))
               constructors final_ty))
@@ -296,14 +298,14 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
       let consno = ref (conslen + 1) in
       let eliminator_body =
         let fix = Cic.Rel (rightno + 2) in
-        let is_recursive = recursive_type uri typeno subst constructors in
+        let is_recursive = recursive_type uri typeno constructors in
         let recshift = if is_recursive then 1 else 0 in
         let (_, branches) =
           List.fold_right
             (fun (_, ty) (shift, branches) ->
               let head = Cic.Rel (rightno + shift + 1 + recshift) in
               let b =
-                branch (uri, typeno, subst) false
+                branch (uri, typeno) false
                   (rightno + conslen + 2 + recshift) leftno ty fix head []
               in
               (shift + 1,  b :: branches))
@@ -316,7 +318,7 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
         let body =
           if is_recursive then
             let fixfun =
-              add_right_lambda dependent leftno (conslen + 2) 2 rightno
+              add_right_lambda dependent leftno (conslen + 2) 1 rightno
                 indty mutcase ty
             in
             (* rightno is the decreasing argument, i.e. the argument of
@@ -333,7 +335,7 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
                 decr consno;
                 let p = Cic.Rel !consno in
                 Cic.Lambda (fresh_binder true,
-                  (delta (uri, typeno, subst) dependent leftno !consno
+                  (delta (uri, typeno) dependent leftno !consno
                     constructor p [mk_constructor !consno]),
                   acc))
               constructors body))
@@ -344,6 +346,8 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
 prerr_endline (CicPp.ppterm eliminator_type);
 prerr_endline (CicPp.ppterm eliminator_body);
 *)
+prerr_endline "generato l'eliminatore";
+prerr_endline "inizio type checking";
       let (computed_type, ugraph) =
         try
           CicTypeChecker.type_of_aux' [] [] eliminator_body CicUniv.empty_ugraph
@@ -352,6 +356,8 @@ prerr_endline (CicPp.ppterm eliminator_body);
             "type checker failure while type checking:\n%s\nerror:\n%s"
             (CicPp.ppterm eliminator_body) msg))
       in
+prerr_endline "fine type checking";
+prerr_endline "inizio are convertible";
       if not (fst (CicReduction.are_convertible []
         eliminator_type computed_type ugraph))
       then