SHARE
TWEET

Untitled

a guest Jun 16th, 2019 59 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. (* A verison of WcbvEval with values as a separate inductive type  *)
  2. From Coq Require Import Bool String List Program BinPos Compare_dec Omega.
  3. From Template Require Import config utils univ BasicAst.
  4. From PCUIC Require Import PCUICAst PCUICAstUtils PCUICInduction PCUICLiftSubst PCUICUnivSubst PCUICTyping.
  5. Require Import String.
  6. Local Open Scope string_scope.
  7. Set Asymmetric Patterns.
  8.  
  9. Existing Instance default_checker_flags.
  10.  
  11. (** * Weak (head) call-by-value evaluation strategy. *)
  12.  
  13. (** ** Big step version of weak cbv beta-zeta-iota-fix-delta reduction. *)
  14.  
  15.  (* TODO: CoFixpoints *)
  16.  
  17.   Inductive value :=
  18.   | vpRel : nat -> value
  19.   | vpEvar : nat -> list term -> value
  20.   | vpLambda : name -> term -> term -> value
  21.   | vpFix : mfixpoint term -> nat -> value
  22.   | vpProd : name -> term -> term -> value
  23.   | vpInd : inductive -> universe_instance -> list value -> value
  24.   | vpConstruct : inductive -> nat -> universe_instance -> list value -> value.
  25.  
  26.  
  27.   Fixpoint value_to_term (v : value): term :=
  28.     match v with
  29.     | vpRel i => tRel i
  30.     | vpEvar x x0 => tEvar x x0
  31.     | vpLambda x x0 x1 => tLambda x x0 x1
  32.     | vpFix mfix n => tFix mfix n
  33.     | vpProd x x0 x1 => tProd x x0 x1
  34.     | vpInd ind u vs => mkApps (tInd ind u) (map value_to_term vs)
  35.     | vpConstruct ind n u vs => mkApps (tConstruct ind n u) (map value_to_term vs)
  36.     end.
  37.  
  38.   Notation "'terms' ts" := (map value_to_term ts) (at level 50).
  39.  
  40.   Definition is_vcontructor (v : value):=
  41.     match v with
  42.     | vpConstruct _ _ _ _ => true
  43.     | _ => false
  44.     end.
  45.  
  46. Section Wcbv.
  47.  
  48.   Open Scope list.
  49.   Context (Σ : global_declarations) (Γ : context).
  50.   (* The local context is fixed: we are only doing weak reductions *)
  51.  
  52.     Inductive eval : term -> value -> Prop :=
  53.   (** Reductions *)
  54.   (** Beta *)
  55.   | eval_beta f na t b a a' res :
  56.       eval f (vpLambda na t b) ->
  57.       eval a a' ->
  58.       eval (subst10 (value_to_term a') b) res ->
  59.       eval (tApp f a) res
  60.  
  61.   (** Let *)
  62.   | eval_zeta na b0 b0' t b1 res :
  63.       eval b0 b0' ->
  64.       eval (subst10 (value_to_term b0') b1) res ->
  65.       eval (tLetIn na b0 t b1) res
  66.  
  67.   (** Local variables: defined or undefined *)
  68.   | eval_rel_def i (isdecl : i < List.length Γ) body res :
  69.       (safe_nth Γ (exist _ i isdecl)).(decl_body) = Some body ->
  70.       eval (lift0 (S i) body) res ->
  71.       eval (tRel i) res
  72.  
  73.   | eval_rel_undef i (isdecl : i < List.length Γ) :
  74.       (safe_nth Γ (exist _ i isdecl)).(decl_body) = None ->
  75.       eval (tRel i) (vpRel i)
  76.  
  77.   (** Case *)
  78.   | eval_iota ind pars discr c u args p brs res :
  79.       eval discr (vpConstruct ind c u args) ->
  80.       eval (iota_red pars c (terms args) brs) res ->
  81.       eval (tCase (ind, pars) p discr brs) res
  82.   (** Fix unfolding, with guard *)
  83.   (* assuming that the fixpoint is defined by recursion of the first arg *)
  84.  
  85.   | eval_fix idx mfix f fn b a v res :
  86.       eval f (vpFix mfix idx) ->
  87.       unfold_fix mfix idx = Some (0, fn) ->
  88.       eval a v ->
  89.       is_vcontructor v = true ->
  90.       eval (subst10 (value_to_term v) b) res ->
  91.       eval (tApp f a) res
  92.  
  93.   (** Constant unfolding *)
  94.   | eval_delta c decl body (isdecl : declared_constant Σ c decl) u res :
  95.       decl.(cst_body) = Some body ->
  96.       eval (subst_instance_constr u body) res ->
  97.       eval (tConst c u) res
  98.  
  99.   (** Proj *)
  100.   (* Not sure about this *)
  101.   (* | eval_proj i pars arg discr args k u res : *)
  102.   (*     eval discr (vpConstruct i k u args) -> *)
  103.   (*     eval (List.nth (pars + arg) args tDummy) res -> *)
  104.   (*     eval (tProj (i, pars, arg) discr) res *)
  105.  
  106.   (* TODO CoFix *)
  107.   | eval_abs na M N : eval (tLambda na M N) (vpLambda na M N)
  108.  
  109.   | eval_prod na b t :
  110.       eval (tProd na b t) (vpProd na b t)
  111.  
  112.   | eval_app_ind t i u a v l :
  113.       eval t (vpInd i u l) ->
  114.       eval a v ->
  115.       eval (tApp t a) (vpInd i u (l ++ [v]))
  116.  
  117.   | eval_tind i u :
  118.       eval (tInd i u) (vpInd i u [])
  119.  
  120.   | eval_app_constr t i k u a v l :
  121.       eval t (vpConstruct i u k l) ->
  122.       eval a v ->
  123.       eval (tApp t a) (vpConstruct i u k (l ++ [v]))
  124.  
  125.   | eval_constr i u k:
  126.       eval (tConstruct i u k) (vpConstruct i u k []).
  127.  
  128.  
  129. End Wcbv.
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top