From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 13 Jan 2005 07:08:55 +0000 (+0000)
Subject: snapshot (1st commit of fix body generation)
X-Git-Tag: V_0_1_0~139
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=086099d1a60948454cf0874744ef2222c2edc1b6;p=helm.git

snapshot (1st commit of fix body generation)
---

diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml
index 77304c1ec..28a8ed31b 100644
--- a/helm/ocaml/cic_proof_checking/cicElim.ml
+++ b/helm/ocaml/cic_proof_checking/cicElim.ml
@@ -33,11 +33,13 @@ let fresh_binder =
         Cic.Name ("elim" ^ string_of_int !counter)
     | _ -> Cic.Anonymous
 
-  (** verifies if a given uri occurs in a term in target position *)
-let rec recursive uri = function
-  | Cic.Prod (_, _, target) -> recursive uri target
-  | Cic.MutInd (uri', _, _) -> UriManager.eq uri uri'
-  | Cic.Appl args -> List.exists (recursive uri) args
+  (** 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 *)
   | _ -> false
 
 let unfold_appl = function
@@ -57,7 +59,8 @@ let rec split l n =
 let rec delta (uri, typeno, subst) dependent paramsno consno t p args =
   assert (subst = []);
   match t with
-  | Cic.MutInd (uri', typeno', subst') ->
+  | Cic.MutInd (uri', typeno', subst') when
+    UriManager.eq uri uri' && typeno = typeno' && subst = subst' ->
       if dependent then
         (match args with
         | [] -> assert false
@@ -80,7 +83,7 @@ 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 src then
+      if recursive uri typeno subst src then
         let args = List.map (CicSubstitution.lift 2) args in
         let phi =
           let src = CicSubstitution.lift 1 src in
@@ -166,6 +169,21 @@ let rec add_right_pi dependent strip liftno liftfrom rightno indty = function
           else
             Cic.Appl (Cic.Rel (1 + liftno + rightno) :: mk_rels 1 rightno))
 
+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,
+        add_right_lambda dependent strip liftno (liftfrom + 1) rightno indty
+          case tgt)
+  | Cic.Prod (_, _, tgt) ->
+      add_right_lambda dependent (strip - 1) liftno liftfrom rightno indty
+        case tgt
+  | t ->
+      Cic.Lambda (fresh_binder true,
+        CicSubstitution.lift_from (rightno + 1) liftno indty,
+        case)
+
 exception Failure of string
 
 let string_of_sort = function
@@ -185,6 +203,7 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
         with Failure _ -> assert false
       in
       let paramsno = count_pi ty in (* number of (left or right) parameters *)
+      let rightno = paramsno - leftno in
       let dependent = (strip_pi ty <> Cic.Sort Cic.Prop) in
       let conslen = List.length constructors in
       let consno = ref (conslen + 1) in
@@ -208,8 +227,7 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
       let eliminator =
         let p_ty = type_of_p sort dependent leftno indty ty in
         let final_ty =
-          add_right_pi dependent leftno (conslen + 1) 1 (paramsno - leftno)
-            indty ty
+          add_right_pi dependent leftno (conslen + 1) 1 rightno indty ty
         in
         Cic.Prod (Cic.Name "P", p_ty,
           (List.fold_right
@@ -220,8 +238,121 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
                 (delta (uri, typeno, subst) dependent leftno !consno
                   constructor p [mk_constructor !consno]),
                 acc))
-            constructors
-            final_ty))
+            constructors final_ty))
+      in
+      add_params leftno ty eliminator
+  | _ -> assert false
+
+let rec branch (uri, typeno, subst) insource paramsno t fix head args =
+  assert (subst = []);
+  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' ->
+      let (lparams, rparams) = split tl paramsno in
+      (match args with
+      | [] when insource && rparams = [] -> fix
+      | [] when insource -> Cic.Appl (fix :: rparams)
+      | _ when insource -> Cic.Appl (fix :: rparams @ args)
+      | _ -> Cic.Appl (head :: rparams @ args))
+  | Cic.Prod (binder, src, tgt) ->
+      if recursive uri typeno subst src then
+        let args = List.map (CicSubstitution.lift 1) args in
+        let phi =
+          let fix = CicSubstitution.lift 1 fix in
+          branch (uri, typeno, subst) true paramsno src fix head
+            (args @ [Cic.Rel 1])
+        in
+        let tgt = CicSubstitution.lift 1 tgt in
+        Cic.Lambda (fresh_binder true, src,
+          branch (uri, typeno, subst) 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
+          (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 t = strip_left_params liftno paramsno t in
+  branch (uri, typeno, subst) insource paramsno t fix head args
+
+let body_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) =
+        try
+          List.nth indTypes typeno
+        with Failure _ -> assert false
+      in
+      let paramsno = count_pi ty in (* number of (left or right) parameters *)
+      let rightno = paramsno - leftno in
+      let dependent = (strip_pi ty <> Cic.Sort Cic.Prop) in
+      let conslen = List.length constructors in
+      let consno = ref (conslen + 1) in
+      if (not dependent) && (sort <> Cic.Prop) && (conslen > 1) then
+        raise (Failure (sprintf "can't eliminate from Prop to %s"
+          (string_of_sort sort)));
+      let indty =
+        let indty = Cic.MutInd (uri, typeno, subst) 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
+        if leftno = 0 then
+          constructor
+        else
+          Cic.Appl (constructor :: mk_rels consno leftno)
+      in
+      let eliminator =
+        let p_ty = type_of_p sort dependent leftno indty ty in
+        let final_ty =
+          add_right_pi dependent leftno (conslen + 1) 1 rightno indty ty
+        in
+        let fix = Cic.Rel (rightno + 2) in
+        let (_, branches) =
+          List.fold_right
+            (fun (_, ty) (shift, branches) ->
+              let head = Cic.Rel (rightno + shift + 2) in
+              let b =
+                branch (uri, typeno, subst) false (rightno + conslen + 3) leftno
+                  ty fix head []
+              in
+              (shift + 1,  b :: branches))
+            constructors (1, [])
+        in
+        let case =
+          Cic.MutCase (uri, typeno, Cic.Rel (conslen + rightno + 3), Cic.Rel 1,
+            branches)
+        in
+        let fix_body =
+          add_right_lambda dependent leftno (conslen + 1) 1 rightno
+            indty case ty
+        in
+        let fix = Cic.Fix (0, ["f", 0, final_ty, fix_body]) in
+        Cic.Lambda (Cic.Name "P", p_ty,
+          (List.fold_right
+            (fun (_, constructor) acc ->
+              decr consno;
+              let p = Cic.Rel !consno in
+              Cic.Lambda (fresh_binder true,
+                (delta (uri, typeno, subst) dependent leftno !consno
+                  constructor p [mk_constructor !consno]),
+                acc))
+            constructors fix))
       in
       add_params leftno ty eliminator
   | _ -> assert false
diff --git a/helm/ocaml/cic_proof_checking/cicElim.mli b/helm/ocaml/cic_proof_checking/cicElim.mli
index b341d36a4..015b6c9d1 100644
--- a/helm/ocaml/cic_proof_checking/cicElim.mli
+++ b/helm/ocaml/cic_proof_checking/cicElim.mli
@@ -29,6 +29,12 @@ exception Failure of string
 * @param uri inductive type uri
 * @param typeno inductive type number
 * @raise Failure
+* @return type of elimination principle for the given inductive type
 *)
 val elim_of: ?sort:Cic.sort -> UriManager.uri -> int -> Cic.term
 
+(** parameters as above
+* @return body of elimination principle for the given inductive type
+*)
+val body_of: ?sort:Cic.sort -> UriManager.uri -> int -> Cic.term
+