- lazy (reduce config), lazy (unwind config)
- end
-;;
-
-
-(* {{{ module CallByValueByNameForUnwind =
- struct
- type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
- and stack_term = config
- and env_term = config * config (* cbv, cbn *)
- and ens_term = config * config (* cbv, cbn *)
-
- let to_env c = c,c
- let to_ens c = c,c
- let from_stack config = config
- let from_stack_list_for_unwind ~unwind l = List.map unwind l
- let from_env (c,_) = c
- let from_ens (c,_) = c
- let from_env_for_unwind ~unwind (_,c) = unwind c
- let from_ens_for_unwind ~unwind (_,c) = unwind c
- let stack_to_env ~reduce ~unwind config = reduce config, (0,[],[],unwind config,[])
- let compute_to_env ~reduce ~unwind k e ens t = (k,e,ens,t,[]), (k,e,ens,t,[])
- let compute_to_stack ~reduce ~unwind config = config
- end
-;;
-
-
-(* Old Machine *)
-module CallByNameStrategy =
- struct
- type stack_term = Cic.term
- type env_term = Cic.term
- type ens_term = Cic.term
- type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
- let to_env v = v
- let to_ens v = v
- let from_stack ~unwind v = v
- let from_stack_list ~unwind l = l
- let from_env v = v
- let from_ens v = v
- let from_env_for_unwind ~unwind v = v
- let from_ens_for_unwind ~unwind v = v
- let stack_to_env ~reduce ~unwind v = v
- let compute_to_stack ~reduce ~unwind k e ens t = unwind k e ens t
- let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t
- end
-;;
-
-module CallByNameStrategy =
- struct
- type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
- and stack_term = config
- and env_term = config
- and ens_term = config
-
- let to_env c = c
- let to_ens c = c
- let from_stack config = config
- let from_stack_list_for_unwind ~unwind l = List.map unwind l
- let from_env c = c
- let from_ens c = c
- let from_env_for_unwind ~unwind c = unwind c
- let from_ens_for_unwind ~unwind c = unwind c
- let stack_to_env ~reduce ~unwind config = 0,[],[],unwind config,[]
- let compute_to_env ~reduce ~unwind k e ens t = k,e,ens,t,[]
- let compute_to_stack ~reduce ~unwind config = config
- end
-;;
-
-module CallByValueStrategy =
- struct
- type stack_term = Cic.term
- type env_term = Cic.term
- type ens_term = Cic.term
- type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
- let to_env v = v
- let to_ens v = v
- let from_stack ~unwind v = v
- let from_stack_list ~unwind l = l
- let from_env v = v
- let from_ens v = v
- let from_env_for_unwind ~unwind v = v
- let from_ens_for_unwind ~unwind v = v
- let stack_to_env ~reduce ~unwind v = v
- let compute_to_stack ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
- let compute_to_env ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
- end
-;;
-
-module CallByValueStrategyByNameOnConstants =
- struct
- type stack_term = Cic.term
- type env_term = Cic.term
- type ens_term = Cic.term
- type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
- let to_env v = v
- let to_ens v = v
- let from_stack ~unwind v = v
- let from_stack_list ~unwind l = l
- let from_env v = v
- let from_ens v = v
- let from_env_for_unwind ~unwind v = v
- let from_ens_for_unwind ~unwind v = v
- let stack_to_env ~reduce ~unwind v = v
- let compute_to_stack ~reduce ~unwind k e ens =
- function
- Cic.Const _ as t -> unwind k e ens t
- | t -> reduce (k,e,ens,t,[])
- let compute_to_env ~reduce ~unwind k e ens =
- function
- Cic.Const _ as t -> unwind k e ens t
- | t -> reduce (k,e,ens,t,[])
- end
-;;
-
-module LazyCallByValueStrategy =
- struct
- type stack_term = Cic.term lazy_t
- type env_term = Cic.term lazy_t
- type ens_term = Cic.term lazy_t
- type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
- let to_env v = lazy v
- let to_ens v = lazy v
- let from_stack ~unwind v = Lazy.force v
- let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
- let from_env v = Lazy.force v
- let from_ens v = Lazy.force v
- let from_env_for_unwind ~unwind v = Lazy.force v
- let from_ens_for_unwind ~unwind v = Lazy.force v
- let stack_to_env ~reduce ~unwind v = v
- let compute_to_stack ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
- let compute_to_env ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))